mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
⊢ ∀ a ∈ antidiagonal (optionElim k x),
    ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x

pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
⊢ ∀ a₁ ∈ antidiagonal (optionElim k x),
    ∀ a₂ ∈ antidiagonal (optionElim k x),
      ⟨(a₁.1 none, a₁.2 none), (a₁.1.some, a₁.2.some)⟩ = ⟨(a₂.1 none, a₂.2 none), (a₂.1.some, a₂.2.some)⟩ → a₁ = a₂

pp: case refine_3
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
⊢ ∀ b ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x,
    ∃ a, ∃ (_ : a ∈ antidiagonal (optionElim k x)), ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩ = b

pp: case refine_4
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
⊢ ∀ a ∈ antidiagonal (optionElim k x),
    (coeff a.1) p * (coeff a.2) q =
      (coeff
            (optionElim ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.fst.1
              ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.snd.1))
          p *
        (coeff
            (optionElim ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.fst.2
              ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.snd.2))
          q

Tactic:
· intros; simp_all [Finsupp.ext_iff]

Goal state after:
case refine_2
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
⊢ ∀ a₁ ∈ antidiagonal (optionElim k x),
    ∀ a₂ ∈ antidiagonal (optionElim k x),
      ⟨(a₁.1 none, a₁.2 none), (a₁.1.some, a₁.2.some)⟩ = ⟨(a₂.1 none, a₂.2 none), (a₂.1.some, a₂.2.some)⟩ → a₁ = a₂

case refine_3
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
⊢ ∀ b ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x,
    ∃ a, ∃ (_ : a ∈ antidiagonal (optionElim k x)), ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩ = b

case refine_4
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
⊢ ∀ a ∈ antidiagonal (optionElim k x),
    (coeff a.1) p * (coeff a.2) q =
      (coeff
            (optionElim ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.fst.1
              ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.snd.1))
          p *
        (coeff
            (optionElim ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.fst.2
              ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.snd.2))
          q
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case refine_4
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
⊢ ∀ a ∈ antidiagonal (optionElim k x),
    (coeff a.1) p * (coeff a.2) q =
      (coeff
            (optionElim ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.fst.1
              ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.snd.1))
          p *
        (coeff
            (optionElim ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.fst.2
              ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.snd.2))
          q

Tactic:
· intros; simp_all [Finsupp.ext_iff]

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

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

Tactic:
rw [toMvPowerSeries_apply, MvPowerSeries.rename_eq_subst, subst_X_comp_const,
    coeff_subst (HasSubst.X _), finsum_eq_zero_of_forall_eq_zero]

Goal state after:
σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
d : σ →₀ ℕ
hd : d i = 0
hf : constantCoeff f = 0
⊢ ∀ (x : ℕ), (coeff x) f • (MvPowerSeries.coeff d) (MvPowerSeries.X i ^ x) = 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case h.h
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.quotientToCoinvariants S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.quotientToCoinvariants S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x)
z : ↥(cycles₁ (res S.subtype (A.toCoinvariants S)))
hz :
  (ModuleCat.Hom.hom (map S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))) 1))
      ((ConcreteCategory.hom (H1π (res S.subtype (A.toCoinvariants S)))) z) =
    (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
⊢ (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1CoresCoinf A S).f).range

Tactic:
rw [H1π_comp_map_apply] at hz

Goal state after:
case h.h
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.quotientToCoinvariants S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.quotientToCoinvariants S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x)
z : ↥(cycles₁ (res S.subtype (A.toCoinvariants S)))
hz :
  (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) =
    (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
⊢ (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1CoresCoinf A S).f).range
Module: Mathlib.RingTheory.Bialgebra.SymmetricAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ↑(TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul

Tactic:
have h : (Algebra.TensorProduct.comm R (SymmetricAlgebra R M)
          (SymmetricAlgebra R M)).toAlgHom.comp (Bialgebra.comulAlgHom R _) =
        Bialgebra.comulAlgHom R (SymmetricAlgebra R M) := by
      ext x
      simp
      abel

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  (↑(Algebra.TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M))).comp
      (Bialgebra.comulAlgHom R (SymmetricAlgebra R M)) =
    Bialgebra.comulAlgHom R (SymmetricAlgebra R M)
⊢ ↑(TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul
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
a : M
b : A
c : M
d : A
⊢ (((LinearMap.mul R A[M]).compr₂ comul ∘ₗ lsingle a) b ∘ₗ lsingle c) d =
    (((LinearMap.mul R (A[M] ⊗[R] A[M])).compl₁₂ comul comul ∘ₗ lsingle a) b ∘ₗ lsingle c) d

Tactic:
simp only [Function.comp_apply, LinearMap.coe_comp, LinearMap.compr₂_apply,
      LinearMap.mul_apply', single_mul_single, comul_single, Bialgebra.comul_mul,
      ← (Coalgebra.Repr.arbitrary R b).eq, ← (Coalgebra.Repr.arbitrary R d).eq, Finset.sum_mul_sum,
      Algebra.TensorProduct.tmul_mul_tmul, map_sum, TensorProduct.map_tmul, lsingle_apply,
      LinearMap.compl₁₂_apply, LinearMap.coe_sum, Finset.sum_apply,
      Finset.sum_comm (s := (Coalgebra.Repr.arbitrary R b).index)]

Goal state after:
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
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) = (valuation K v) ↑x

Tactic:
show v.valuation K x = _ * _ by rw [valuation_def]; rfl

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
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) =
    ↑v.intValuation.toMonoidWithZeroHom ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1 *
      ↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).domRestrict R⁰) ⋯)
            ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2)⁻¹
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case pos
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
f : A →+* B
hIJ : map f I ≤ J
H : ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
hn : n = 0
⊢ ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)

Tactic:
intro _ ha
    rw [hn, hI.dpow_zero ha, hJ.dpow_zero (hIJ (mem_map_of_mem f ha)), map_one]

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 ∈ (insert a s).sym n, (Sym.filterNe a m).snd ∈ s.sym (n - ↑(Sym.filterNe a m).fst)

Tactic:
intro m hm
      convert! sym_filterNe_mem a hm
      rw [erase_insert ha]

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
S : Type u_4
inst✝³ : CommSemiring S
N : Type u_5
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Module S N
f : M →ₗ[R] N
n : ℕ
a b : M
⊢ dp S n (f (a + b)) = ∑ k ∈ antidiagonal n, dp S k.1 (f a) * dp S k.2 (f b)

Tactic:
rw [map_add, DividedPowerAlgebra.dp_add]

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

Goal state before:
pp: case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
aux : ↑n ! = ↑n ! • 1
⊢ ¬↑n ! = ↑0

Tactic:
simp [factorial_ne_zero]

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

Goal state before:
pp: case refine_1
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
y : A
m : ℕ
hm : m ≠ 0
x : A
hxS : x ∈ S
hxy : y = hI.dpow m x
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n y ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
rw [hxy, hI.dpow_comp hm (hS hxS)]

Goal state after:
case refine_1
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
y : A
m : ℕ
hm : m ≠ 0
x : A
hxS : x ∈ S
hxy : y = hI.dpow m x
n : ℕ
hn : n ≠ 0
⊢ ↑(n.uniformBell m) * hI.dpow (n * m) x ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
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✝ : IsFiniteSplit k R
p : PrimeSpectrum R
⊢ Ideal.comap (Ideal.Quotient.mkₐ k p.asIdeal) (RingHom.ker ↑(AlgEquiv.ofBijective (ofId k (R ⧸ p.asIdeal)) ⋯).symm) =
    p.asIdeal

Tactic:
AlgHom.ker_coe_equiv,

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✝ : IsFiniteSplit k R
p : PrimeSpectrum R
⊢ Ideal.comap (Ideal.Quotient.mkₐ k p.asIdeal) ⊥ = p.asIdeal
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case h
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
u : R⟦X⟧ˣ
⊢ (heval x) ↑u * (heval x) u.inv = 1

Tactic:
rw [← heval_mul, Units.val_inv, map_one]

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 : Γ × Γ'
a✝ : α × β
hab : a✝ ∈ Function.support fun i ↦ (s i.1).coeff gh.1 • (t i.2).coeff gh.2
⊢ a✝ ∈ ↑⋯.toFinset

Tactic:
simp_all only [Function.mem_support, ne_eq, Set.Finite.coe_toFinset, Set.mem_prod,
    Set.mem_ofPred_eq]

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✝³ : PartialOrder Γ'
inst✝² : AddCommMonoid V
inst✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
gh : Γ × Γ'
a✝ : α × β
hab : ¬(s a✝.1).coeff gh.1 • (t a✝.2).coeff gh.2 = 0
⊢ ¬(s.toFun a✝.1).coeff gh.1 = 0 ∧ ¬(t.toFun a✝.2).coeff gh.2 = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

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

Tactic:
by
      have : PowerSeries.HasSubst (subst ![PowerSeries.X (R := R), 0] F.toPowerSeries) := by
        refine PowerSeries.HasSubst.of_constantCoeff_zero' ?_
        rw [PowerSeries.constantCoeff, PowerSeries.X, constantCoeff_subst_eq_zero HasSubst.X_zero
          (by simp) F.zero_constantCoeff]
      rw [PowerSeries.subst, subst_comp_subst_apply _ this.const]
      · congr! 2 with d
        fin_cases d
        · simp [← PowerSeries.subst_def, PowerSeries.subst_X this]
        · simp [← PowerSeries.subst_def, ← PowerSeries.coe_substAlgHom this]
      · exact HasSubst.X_zero

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ ∑ᶠ (i : α × β), ∑ x ∈ VAddAntidiagonal g ⋯, (s i.1).coeff x.1 • (t i.2).coeff x.2 =
    ∑ x ∈ VAddAntidiagonal g ⋯,
      ∑ x_1 ∈ (t.coeff x.2).support, ∑ i ∈ (s.coeff x.1).support, (s i).coeff x.1 • (t x_1).coeff x.2

Tactic:
← sum_finsum_comm _ _ <| fun gh _ => hasFiniteSupport_smul s t gh

Goal state after:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ ∑ a ∈ VAddAntidiagonal g ⋯, ∑ᶠ (b : α × β), (s b.1).coeff a.1 • (t b.2).coeff a.2 =
    ∑ x ∈ VAddAntidiagonal g ⋯,
      ∑ x_1 ∈ (t.coeff x.2).support, ∑ i ∈ (s.coeff x.1).support, (s i).coeff x.1 • (t x_1).coeff x.2
Module: Mathlib.RingTheory.FormalGroup.Basic

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

Tactic:
have : PowerSeries.HasSubst (subst ![0, PowerSeries.X (R := R)] F.toPowerSeries) := by
        refine PowerSeries.HasSubst.of_constantCoeff_zero' ?_
        rw [PowerSeries.constantCoeff, PowerSeries.X, constantCoeff_subst_eq_zero HasSubst.zero_X
          (by simp) F.zero_constantCoeff]

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![0, PowerSeries.X] F.toPowerSeries)
⊢ PowerSeries.subst F.zeroX F.zeroX = subst ![0, subst ![0, PowerSeries.X] F.toPowerSeries] F.toPowerSeries
Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding

Goal state before:
pp: M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
⊢ ∃ f,
    Function.Injective ⇑f ∧
      ∀ (a : M), ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (f a)).orderTop

Tactic:
let f₁ := DivisibleHull.coeOrderAddMonoidHom M

Goal state after:
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
⊢ ∃ f,
    Function.Injective ⇑f ∧
      ∀ (a : M), ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (f a)).orderTop
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : Invertible ((PowerSeries.coeff 1) F.zeroX)
⊢ F.zeroX = PowerSeries.subst (PowerSeries.subst F.zeroX F.zeroX) F.zeroX.substInv

Tactic:
have aux₀ : PowerSeries.HasSubst F.zeroX :=
        PowerSeries.HasSubst.of_constantCoeff_zero' <| F.constantCoeff_zeroX
      rw [← PowerSeries.subst_comp_subst_apply aux₀ aux₀, PowerSeries.subst_substInv_left _
        F.constantCoeff_zeroX, PowerSeries.subst_X aux₀, zeroX]

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
f : α →₀ R⟦Γ⟧
a : α
g : Γ
hg : g ∈ (f a).support
haf : a ∈ f.support
⊢ g ∈ ⋃ i ∈ f.support, (f i).support

Tactic:
exact Set.mem_biUnion haf hg

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

Goal state before:
pp: case pos
Γ : 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 α
f : α ↪ β
g : Γ
b : β
h : b ∈ {a | (if h : a ∈ Set.range ⇑f then s (Classical.choose h) else 0).coeff g ≠ 0}
hb : b ∈ Set.range ⇑f
⊢ b ∈ ⇑f '' Function.support fun a ↦ (s a).coeff g

Tactic:
simp only [Ne, Set.mem_ofPred_eq, dif_pos hb] at h

Goal state after:
case pos
Γ : 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 α
f : α ↪ β
g : Γ
b : β
hb : b ∈ Set.range ⇑f
h : ¬(s (Classical.choose hb)).coeff g = 0
⊢ b ∈ ⇑f '' Function.support fun a ↦ (s a).coeff g
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K[X]
x✝¹ : f.Monic
a₀ : K
h₁ : Polynomial.eval a₀ f ∈ maximalIdeal K
x✝ : IsUnit (Polynomial.eval a₀ (derivative f))
⊢ ∃ a, f.IsRoot a ∧ a - a₀ ∈ maximalIdeal K

Tactic:
simp only [(maximalIdeal K).eq_bot_of_prime, Ideal.mem_bot] at h₁ ⊢

Goal state after:
K : Type u_1
inst✝ : Field K
f : K[X]
x✝¹ : f.Monic
a₀ : K
x✝ : IsUnit (Polynomial.eval a₀ (derivative f))
h₁ : Polynomial.eval a₀ f = 0
⊢ ∃ a, f.IsRoot a ∧ a - a₀ = 0
Module: Mathlib.RingTheory.HahnSeries.Cardinal

Goal state before:
pp: Γ : Type u_1
R : Type u_2
S : Type u_3
α : Type u_4
κ : Cardinal.{u_1}
inst✝³ : LinearOrder Γ
inst✝² : AddCommGroup Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
hκ : Fact (ℵ₀ < κ)
x✝¹ : R⟦Γ⟧
x✝ :
  x✝¹ ∈
    (have this := ⋯;
      cardSuppLTSubring Γ R κ).carrier
⊢ max ℵ₀ x✝¹.cardSupp < κ

Tactic:
simpa [hκ.out]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : HasGoingUp R S
inst✝ : HasGoingUp S T
⊢ HasGoingUp R T

Tactic:
iff_specializingMap_primeSpectrumComap,

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : HasGoingUp R S
inst✝ : HasGoingUp S T
⊢ SpecializingMap (PrimeSpectrum.comap (algebraMap R T))
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case hIN.refine_2
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := { toFun := fun n ↦ map (Quotient.mk I) (comap f (map f q ^ n)), monotone' := ⋯ }
n : ℕ
hn : comap f (map f q ^ n) ⊔ I = comap f (map f q ^ n.succ) ⊔ I
x : R
hx :
  x ∈
    (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
      (map (algebraMap R (Localization.AtPrime q)) q ^ n)
⊢ x ∈
    (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q)) (map f q ^ (n + 1)) ⊔
      I •
        (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
          (map (algebraMap R (Localization.AtPrime q)) q ^ n)

Tactic:
obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp (hn.le (Ideal.mem_sup_left hx))

Goal state after:
case hIN.refine_2
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := { toFun := fun n ↦ map (Quotient.mk I) (comap f (map f q ^ n)), monotone' := ⋯ }
n : ℕ
hn : comap f (map f q ^ n) ⊔ I = comap f (map f q ^ n.succ) ⊔ I
y : R
hy : y ∈ comap f (map f q ^ n.succ)
z : R
hz : z ∈ I
hx :
  y + z ∈
    (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
      (map (algebraMap R (Localization.AtPrime q)) q ^ n)
⊢ y + z ∈
    (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q)) (map f q ^ (n + 1)) ⊔
      I •
        (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
          (map (algebraMap R (Localization.AtPrime q)) q ^ n)
Module: Mathlib.RingTheory.Ideal.Pure

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
h : ∀ x ∈ I, ∃ y ∈ I, x = x * y
p : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
x : R
hx : x ∈ I
y : R
hy : y ∈ I
heq : x = x * y
hz : 1 - y ∈ ↑p
⊢ 1 ∈ p

Tactic:
← sub_add_cancel 1 y

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
h : ∀ x ∈ I, ∃ y ∈ I, x = x * y
p : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
x : R
hx : x ∈ I
y : R
hy : y ∈ I
heq : x = x * y
hz : 1 - y ∈ ↑p
⊢ 1 - y + y ∈ p