mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
a✝ : G
x✝ : ↑A
⊢ (ModuleCat.Hom.hom (d₁₀ A) ∘ₗ lsingle a✝) x✝ = (ModuleCat.Hom.hom 0 ∘ₗ lsingle a✝) x✝

Tactic:
simp [d₁₀]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
s : R
hs : s ∈ S
t : R⟦X⟧
htmem : t ∈ T
ht : constantCoeff t = s
⊢ ∃ x ∈ span T, constantCoeff x = s

Tactic:
exact ⟨t, subset_span htmem, ht⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
r₁ r₂ : R
hr₁ : r₁ ∈ Submodule.span R S
hr₂ : r₂ ∈ Submodule.span R S
s₁ : R⟦X⟧
hs₁mem : s₁ ∈ span T
hs₁ : constantCoeff s₁ = r₁
s₂ : R⟦X⟧
hs₂mem : s₂ ∈ span T
hs₂ : constantCoeff s₂ = r₂
⊢ constantCoeff (s₁ + s₂) = r₁ + r₂

Tactic:
simp [hs₁, hs₂]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
⊢ optionFunLeft σ R ((monomial x) r) = (PowerSeries.monomial (x none)) ((monomial x.some) r)

Tactic:
classical
  ext n y
  rw [PowerSeries.coeff_monomial, coeff_coeff_optionFunLeft, coeff_monomial]
  split_ifs with h1 h2 h3
  · simp [← h1]
  · absurd h2
    rw [← optionElim_apply_none n, h1]
  · replace h1 : ¬ y = x.some := fun h ↦ by
      absurd h1; ext u
      cases u <;> simp_all
    rw [coeff_monomial, if_neg h1]
  · rw [coeff_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ contentIdeal 1 = span {1}

Tactic:
← contentIdeal_C 1,

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ contentIdeal 1 = (C 1).contentIdeal
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ p.IsPrimitive ↔ p.contentIdeal = ⊤

Tactic:
refine ⟨?_, fun h ↦ isPrimitive_of_contentIdeal_eq_top h⟩

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ p.IsPrimitive → p.contentIdeal = ⊤
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: case neg.mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
⊢ (∃ x ∈ p.coeffs, 1 ≤ (v.intAdicAbv hb) x) → 1 ≤ p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)

Tactic:
simp only [mem_coeffs_iff, mem_support_iff, ↓existsAndEq, and_true, forall_exists_index,
      and_imp]

Goal state after:
case neg.mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
⊢ ∀ (x : ℕ),
    p.coeff x ≠ 0 → 1 ≤ (v.intAdicAbv hb) (p.coeff x) → 1 ≤ p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: case right
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 inv✝ : R
inv_val✝ : inv✝ * x = 1
hx : v.intValuation x * v.intValuation inv✝ = 1
⊢ 1 ≤ (valuation K v) ((algebraMap R K) x)

Tactic:
← hx,

Goal state after:
case right
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 inv✝ : R
inv_val✝ : inv✝ * x = 1
hx : v.intValuation x * v.intValuation inv✝ = 1
⊢ v.intValuation x * v.intValuation inv✝ ≤ (valuation K v) ((algebraMap R K) x)
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : M
⊢ ↑n ! * dp R n x = dp R 1 x ^ n

Tactic:
induction n with
  | zero => simp [dp_zero]
  | succ n h =>
    rw [pow_succ, ← h, mul_assoc, dp_mul, nsmul_eq_mul, ← mul_assoc, ← Nat.cast_mul]
    simp [mul_comm _ (n + 1), Nat.factorial_succ]

Goal state after:
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
Nfin : Module.Finite R ↑N
Nsupp : Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      ∀ (rs : List R),
        (∀ r ∈ rs, r ∈ I) → RingTheory.Sequence.IsRegular (↑M) rs → rs.length = n → ∀ i < n, Subsingleton (Ext N M i)
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
rs : List R
i✝ : ℕ
le_rad : I ≤ (Module.annihilator R ↑N).radical
a : R
rs' : List R
k : ℕ
hk : a ^ k ∈ Module.annihilator R ↑N
reg : IsSMulRegular (↑M) a ∧ RingTheory.Sequence.IsRegular (QuotSMulTop a ↑M) rs'
mem : a ∈ I ∧ ∀ a ∈ rs', a ∈ I
len : rs'.length = n
i : ℕ
hi : i + 1 < n + 1
g : AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₁ (i + 1)) ⟶
  AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₂ (i + 1)) :=
  AddCommGrpCat.ofHom ((Ext.mk₀ (M.smulShortComplex a).f).postcomp N ⋯)
mono_g : Mono g
⊢ Subsingleton (Ext N M (i + 1))

Tactic:
let gk := AddCommGrpCat.ofHom ((Ext.mk₀ (M.smulShortComplex (a ^ k)).f).postcomp N
          (add_zero (i + 1)))

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
Nfin : Module.Finite R ↑N
Nsupp : Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      ∀ (rs : List R),
        (∀ r ∈ rs, r ∈ I) → RingTheory.Sequence.IsRegular (↑M) rs → rs.length = n → ∀ i < n, Subsingleton (Ext N M i)
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
rs : List R
i✝ : ℕ
le_rad : I ≤ (Module.annihilator R ↑N).radical
a : R
rs' : List R
k : ℕ
hk : a ^ k ∈ Module.annihilator R ↑N
reg : IsSMulRegular (↑M) a ∧ RingTheory.Sequence.IsRegular (QuotSMulTop a ↑M) rs'
mem : a ∈ I ∧ ∀ a ∈ rs', a ∈ I
len : rs'.length = n
i : ℕ
hi : i + 1 < n + 1
g : AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₁ (i + 1)) ⟶
  AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₂ (i + 1)) :=
  AddCommGrpCat.ofHom ((Ext.mk₀ (M.smulShortComplex a).f).postcomp N ⋯)
mono_g : Mono g
gk : AddCommGrpCat.of (Ext N (M.smulShortComplex (a ^ k)).X₁ (i + 1)) ⟶
  AddCommGrpCat.of (Ext N (M.smulShortComplex (a ^ k)).X₂ (i + 1)) :=
  AddCommGrpCat.ofHom ((Ext.mk₀ (M.smulShortComplex (a ^ k)).f).postcomp N ⋯)
⊢ Subsingleton (Ext N M (i + 1))
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: 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
f : A →+* B
hf : map f I ≤ J
a✝ b✝ : A
hx : a✝ ∈ {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}
hy : b✝ ∈ {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}
⊢ a✝ + b✝ ∈ {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}

Tactic:
simp only [mem_ofPred_eq, map_add] at hx hy ⊢

Goal state after:
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
f : A →+* B
hf : map f I ≤ J
a✝ b✝ : A
hx : a✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n a✝) = hJ.dpow n (f a✝)
hy : b✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n b✝) = hJ.dpow n (f b✝)
⊢ a✝ + b✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n (a✝ + b✝)) = hJ.dpow n (f a✝ + f b✝)
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: 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
f : A →+* B
S : Set A
hS : I = span S
hf : map f I ≤ J
h : ∀ {n : ℕ}, ∀ x ∈ S, f (hI.dpow n x) = hJ.dpow n (f x)
n : ℕ
x : A
hx : x ∈ I
hS' : I ≤ hI.ideal_from_ringHom hJ hf
⊢ hJ.dpow n (f x) = f (hI.dpow n x)

Tactic:
exact ((hS' hx).2 n).symm

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

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

Tactic:
simp only [RingEquiv.apply_symm_apply]

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

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ y ^ k.2 * x ^ k.1 ∈ I ^ n

Tactic:
apply Set.mem_of_subset_of_mem h_sub

Goal state after:
case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ y ^ k.2 * x ^ k.1 ∈ ↑(I ^ m)
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case refine_1
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[ε]
hx : x ∈ I
⊢ ε ∣ x

Tactic:
simp_rw [hd _ hx]

Goal state after:
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 R S
⊢ Module.Free R S

Tactic:
obtain ⟨n, ⟨e⟩⟩ := nonempty_algEquiv_fun R S

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 R S
n : ℕ
e : S ≃ₐ[R] Fin n → R
⊢ Module.Free R S
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 R S
⊢ Module.FinitePresentation R S

Tactic:
obtain ⟨n, ⟨e⟩⟩ := nonempty_algEquiv_fun R S

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 R S
n : ℕ
e : S ≃ₐ[R] Fin n → R
⊢ Module.FinitePresentation R S
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 R S
⊢ Etale R S

Tactic:
obtain ⟨n, ⟨e⟩⟩ := nonempty_algEquiv_fun R S

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 R S
n : ℕ
e : S ≃ₐ[R] Fin n → R
⊢ Etale R S
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 (fun s ↦ subst ![f₀, f₁, f₂] (![subst ![Y₀, Y₁] F.toPowerSeries, Y₂] s)) F.toPowerSeries

Tactic:
congr! 2 with s

Goal state after:
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 0).succ
⊢ ![subst ![f₀, f₁] F.toPowerSeries, f₂] s = subst ![f₀, f₁, f₂] (![subst ![Y₀, Y₁] F.toPowerSeries, Y₂] s)
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₂]
⊢ subst ![f₀, f₁] F.toPowerSeries = subst (fun s ↦ subst ![f₀, f₁, f₂] (![Y₀, Y₁] s)) F.toPowerSeries

Tactic:
congr! 2 with s

Goal state after:
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)
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 (fun s ↦ subst ![f₀, f₁, f₂] (![Y₀, subst ![Y₁, Y₂] F.toPowerSeries] s)) F.toPowerSeries =
    subst ![f₀, subst ![f₁, f₂] F.toPowerSeries] F.toPowerSeries

Tactic:
congr! 2 with s

Goal state after:
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 0).succ
⊢ subst ![f₀, f₁, f₂] (![Y₀, subst ![Y₁, Y₂] F.toPowerSeries] s) = ![f₀, subst ![f₁, f₂] F.toPowerSeries] s
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case «1»
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 (fun s ↦ subst ![f₀, f₁, f₂] (![X 1, X 2] s)) F.toPowerSeries = subst ![f₁, f₂] F.toPowerSeries

Tactic:
congr! 2 with s

Goal state after:
case «1»
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 0).succ
⊢ subst ![f₀, f₁, f₂] (![X 1, X 2] s) = ![f₁, f₂] s
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 (fun s ↦ subst ![f, g] (![X 1, X 0] s)) F.toPowerSeries = subst ![g, f] F.toPowerSeries

Tactic:
congr! 2 with s

Goal state after:
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
s : Fin (Nat.succ 0).succ
⊢ subst ![f, g] (![X 1, X 0] s) = ![g, f] s
Module: Mathlib.RingTheory.PowerSeries.Binomial

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
d n : ℕ
hright : (1 + X) ^ d = ↑((1 + Polynomial.X) ^ d)
⊢ (coeff n) (binomialSeries A ↑d) = (coeff n) ↑((1 + Polynomial.X) ^ d)

Tactic:
Polynomial.coeff_coe,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
d n : ℕ
hright : (1 + X) ^ d = ↑((1 + Polynomial.X) ^ d)
⊢ (coeff n) (binomialSeries A ↑d) = ((1 + Polynomial.X) ^ d).coeff n
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
x y : SummableFamily Γ R α
g : Γ
a : α
ha : a ∈ {a | ((⇑x + ⇑y) a).coeff g ≠ 0}
⊢ a ∈ (Function.support fun a ↦ (x a).coeff g) ∪ Function.support fun a ↦ (y a).coeff g

Tactic:
change (x a).coeff g + (y a).coeff g ≠ 0 at ha

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
x y : SummableFamily Γ R α
g : Γ
a : α
ha : (x a).coeff g + (y a).coeff g ≠ 0
⊢ a ∈ (Function.support fun a ↦ (x a).coeff g) ∪ Function.support fun a ↦ (y a).coeff g
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 : Γ'
⊢ (s.smul t).hsum.coeff g = ((of R).symm (s.hsum • (of R) t.hsum)).coeff g

Tactic:
coeff_smul s t g,

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 : Γ'
⊢ ∑ gh ∈ VAddAntidiagonal g ⋯, s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = ((of R).symm (s.hsum • (of R) t.hsum)).coeff g
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ subst ![f, 0] F.toPowerSeries = subst (fun s ↦ subst (fun x ↦ f) (![PowerSeries.X, 0] s)) F.toPowerSeries

Tactic:
congr! 2 with s

Goal state after:
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
s : Fin (Nat.succ 0).succ
⊢ ![f, 0] s = subst (fun x ↦ f) (![PowerSeries.X, 0] s)
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ subst ![0, f] F.toPowerSeries = subst (fun s ↦ subst (fun x ↦ f) (![0, PowerSeries.X] s)) F.toPowerSeries

Tactic:
congr! 2 with s

Goal state after:
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
s : Fin (Nat.succ 0).succ
⊢ ![0, f] s = subst (fun x ↦ f) (![0, PowerSeries.X] s)
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
s : SummableFamily Γ R α
t : SummableFamily Γ R β
⊢ (s.mul t).hsum = s.hsum * t.hsum

Tactic:
rw [← smul_eq_mul, mul_eq_smul]

Goal state after:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
s : SummableFamily Γ R α
t : SummableFamily Γ R β
⊢ (s.smul t).hsum = s.hsum • t.hsum
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (↑f).toLinearMap ∘ₗ (toConv (antipode R) * toConv LinearMap.id).ofConv = ofConv 1 ∘ₗ f.toLinearMap

Tactic:
rw [antipode_mul_id, algHom_comp_convOne, ← convOne_comp_coalgHom f.toCoalgHom]

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

Goal state before:
pp: case neg.refine_2
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : WfDvdMonoid R
x : R
hx : Prime x
p : Ideal R
inst✝³ : p.IsPrime
hxp : x ∉ p
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization.Away x S
this : Disjoint ↑(Submonoid.powers x) ↑p
hpbot : ¬p = ⊥
hi : Function.Injective ⇑(algebraMap R S)
hpb : map (algebraMap R S) p ≠ ⊥
g : S
hg : map (algebraMap R S) p = S ∙ g
hg0 : g ≠ 0
a : R
n : ℤ
hxa : ¬x ∣ a
hag : selfZPow x S n * (algebraMap R S) a = g
hu : IsUnit (selfZPow x S n)
⊢ ∀ (y : R), x * y ∈ R ∙ a → y ∈ R ∙ a

Tactic:
intro y hy

Goal state after:
case neg.refine_2
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : WfDvdMonoid R
x : R
hx : Prime x
p : Ideal R
inst✝³ : p.IsPrime
hxp : x ∉ p
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization.Away x S
this : Disjoint ↑(Submonoid.powers x) ↑p
hpbot : ¬p = ⊥
hi : Function.Injective ⇑(algebraMap R S)
hpb : map (algebraMap R S) p ≠ ⊥
g : S
hg : map (algebraMap R S) p = S ∙ g
hg0 : g ≠ 0
a : R
n : ℤ
hxa : ¬x ∣ a
hag : selfZPow x S n * (algebraMap R S) a = g
hu : IsUnit (selfZPow x S n)
y : R
hy : x * y ∈ R ∙ a
⊢ y ∈ R ∙ a
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
q p : Ideal R
inst✝ : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : p ∈ (span (insert x s)).minimalPrimes
t : Set R
htq : t ⊆ ↑q
hsp : s ⊆ ↑(span (insert x t)).radical
f : R →+* R ⧸ span t := Quotient.mk (span t)
hf : Function.Surjective ⇑f
hI'q : span t ≤ q
hI'p : span t ≤ p
this✝ : p.IsPrime
this : (map f p).IsPrime
h : (map f p).height ≤ 1
h_lt : map f q < map f p
⊢ q ∈ (span t).minimalPrimes

Tactic:
have : (q.map f).IsPrime := map_isPrime_of_surjective hf (by rwa [mk_ker])

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
q p : Ideal R
inst✝ : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : p ∈ (span (insert x s)).minimalPrimes
t : Set R
htq : t ⊆ ↑q
hsp : s ⊆ ↑(span (insert x t)).radical
f : R →+* R ⧸ span t := Quotient.mk (span t)
hf : Function.Surjective ⇑f
hI'q : span t ≤ q
hI'p : span t ≤ p
this✝¹ : p.IsPrime
this✝ : (map f p).IsPrime
h : (map f p).height ≤ 1
h_lt : map f q < map f p
this : (map f q).IsPrime
⊢ q ∈ (span t).minimalPrimes
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ p.height ≤ Cardinal.toENat (Submodule.spanRank I)

Tactic:
rw [I.spanRank_toENat_eq_iInf_finset_card, le_iInf_iff]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ ∀ (i : { s // Submodule.span R ↑s = I }), p.height ≤ ↑(↑i).card