mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Regular.RegularSequence

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

Tactic:
refine absurd ?_ (ne_of_lt (lt_of_le_of_lt le_sup_left h.right))

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
rs : List R
h : (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs) ∧ r • ⊤ ⊔ Ideal.ofList rs • ⊤ < ⊤
⊢ r • ⊤ = ⊤
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
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ (↑m !)⁻¹ʳ * ((↑k !)⁻¹ʳ * (x ^ m * x ^ k)) = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * x ^ (m + k))

Tactic:
← pow_add,

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ (↑m !)⁻¹ʳ * ((↑k !)⁻¹ʳ * x ^ (m + k)) = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * x ^ (m + k))
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 k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ (↑m !)⁻¹ʳ * ((↑k !)⁻¹ʳ * (x ^ m * x ^ k)) = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * x ^ (m + k))

Tactic:
← pow_add,

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 k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ (↑m !)⁻¹ʳ * ((↑k !)⁻¹ʳ * x ^ (m + k)) = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * x ^ (m + k))
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: case hbc
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hx0 : ¬x = 0
hlt : ↑(padicValNat p n !) < ↑n
hnorm : 0 < ‖↑n !‖
⊢ 1 ≤ x.valuation

Tactic:
← PadicInt.mem_span_pow_iff_le_valuation x hx0,

Goal state after:
case hbc
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hx0 : ¬x = 0
hlt : ↑(padicValNat p n !) < ↑n
hnorm : 0 < ‖↑n !‖
⊢ x ∈ Ideal.span {↑p ^ 1}
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hn : ¬n = 0
⊢ 1 ≤ ↑p

pp: case hmn
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hn : ¬n = 0
⊢ -1 ≤ 0

Tactic:
· exact_mod_cast Nat.Prime.one_le hp.elim

Goal state after:
case hmn
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hn : ¬n = 0
⊢ -1 ≤ 0
Module: Mathlib.RingTheory.DualNumber

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

Tactic:
TrivSqZeroExt.snd_mul,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ TrivSqZeroExt.fst x = 0 ↔
    ∃ c,
      TrivSqZeroExt.fst x = TrivSqZeroExt.fst ε * TrivSqZeroExt.fst c ∧
        TrivSqZeroExt.snd x =
          TrivSqZeroExt.fst ε • TrivSqZeroExt.snd c + MulOpposite.op (TrivSqZeroExt.fst c) • TrivSqZeroExt.snd ε
Module: Mathlib.RingTheory.DualNumber

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

Tactic:
exists_and_left,

Goal state after:
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
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
x✝ : ℕ
hn : x✝ ≠ 0
⊢ hI.dpow x✝ 0 ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
by simp only [hI.dpow_eval_zero hn, zero_mem]

Goal state after:
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
⊢ P.cotangentComplex ∘ₗ ↑P.cotangentExtendScalarsEquiv ∘ₗ h1Cotangentι =
    H1Cotangent.δ R P.Ring S ∘ₗ H1Cotangent.map (Hom.ofAlgHom (ofId P.Ring (Generators.self P.Ring S).Ring) ⋯)

Tactic:
ext ⟨x, _⟩

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.extendScalars.Cotangent
property✝ : x ∈ P.extendScalars.cotangentComplex.ker
⊢ (P.cotangentComplex ∘ₗ ↑P.cotangentExtendScalarsEquiv ∘ₗ h1Cotangentι) ⟨x, property✝⟩ =
    (H1Cotangent.δ R P.Ring S ∘ₗ H1Cotangent.map (Hom.ofAlgHom (ofId P.Ring (Generators.self P.Ring S).Ring) ⋯))
      ⟨x, property✝⟩
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: 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}

Tactic:
have h : J ∈ insert ⊤ {J : hI.SubDPIdeal | S ⊆ ↑J.carrier} :=
      Set.mem_insert_of_mem _
        (fun x hx ↦ subset_span ⟨1, one_ne_zero, x, hx, by rw [hI.dpow_one (hS hx)]⟩)

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 :=
  { carrier := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}, isSubideal := ⋯, dpow_mem := ⋯ }
h : J ∈ insert ⊤ {J | S ⊆ ↑J.carrier}
⊢ ⨅ s ∈ insert ⊤ {J | S ⊆ ↑J.carrier}, s.carrier ≤ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
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
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
j : ℕ
⊢ ζ ^ (i * j) - ζ ^ ((q + k - i) * j) * ζ ^ (i * j) ∈ Q

Tactic:
← pow_add,

Goal state after:
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
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
j : ℕ
⊢ ζ ^ (i * j) - ζ ^ ((q + k - i) * j + i * j) ∈ Q
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: case inr
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
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this✝ : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : ζ ^ (q + k - i) * ζ ^ i = ζ ^ i
⊢ φ ζ = ζ ^ q

Tactic:
← pow_add,

Goal state after:
case inr
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
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this✝ : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : ζ ^ (q + k - i + i) = ζ ^ i
⊢ φ ζ = ζ ^ q
Module: Mathlib.RingTheory.GradedAlgebra.AlgHom

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
V : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
ι : Type u_10
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Semiring B
inst✝¹¹ : Semiring C
inst✝¹⁰ : Semiring D
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra R C
inst✝⁶ : Algebra R D
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
𝒞 : ι → Submodule R C
𝒟 : ι → Submodule R D
inst✝³ : GradedAlgebra 𝒜
inst✝² : GradedAlgebra ℬ
inst✝¹ : GradedAlgebra 𝒞
inst✝ : GradedAlgebra 𝒟
f g : 𝒜 →ₐᵍ[R] ℬ
h : (fun f ↦ (↑↑f.toRingHom).toFun) f = (fun f ↦ (↑↑f.toRingHom).toFun) g
⊢ f = g

Tactic:
rcases f with ⟨⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩, _⟩
    rcases g with ⟨⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩, _⟩
    congr

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
G : Type u_3
inst✝³ : Group G
inst✝² : MulSemiringAction G S
inst✝¹ : SMulCommClass G R S
Q : Ideal S
σ : G
inst✝ : Q.IsPrime
h : IsArithFrobAt R σ Q
⊢ σ ∈ MulAction.stabilizer G Q

Tactic:
rw [MulAction.mem_stabilizer_iff]
  conv_lhs => rw [← h.comap_eq]
  rw [Ideal.pointwise_smul_def]
  exact Q.map_comap_eq_self_of_equiv (MulSemiringAction.toRingEquiv G S σ)

Goal state after:
Module: Mathlib.RingTheory.Grassmannian

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
k : ℕ
A : Type w
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A →ₐ[R] B
C : Type w
inst✝¹ : CommRing C
inst✝ : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
⊢ map (g.comp f) N = map g (map f N)

Tactic:
have hfAB : Function.Surjective fAB :=
    (LinearMap.baseChange_surjective B (Submodule.mkQ_surjective _)).comp
      (cancelBaseChange R A B B M).symm.surjective

Goal state after:
R : Type u
inst✝⁸ : CommRing R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
k : ℕ
A : Type w
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A →ₐ[R] B
C : Type w
inst✝¹ : CommRing C
inst✝ : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB : Function.Surjective ⇑fAB
⊢ map (g.comp f) N = map g (map f N)
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: A : Type u_1
A' : Type u_2
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
f : A →+* A'
n✝ : ℕ
⊢ (coeff n✝) ((map f) (cos A)) = (coeff n✝) (cos A')

Tactic:
simp [cos, apply_ite f]

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

Goal state before:
pp: case h
Γ : 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
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
c : ℕ × ℕ
hcn : c.1 + c.2 = n
hc : (PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • (x ^ n).coeff g ≠ 0
⊢ ((PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • (x ^ c.1 * x ^ c.2)).coeff g ≠ 0

Tactic:
← pow_add,

Goal state after:
case h
Γ : 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
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
c : ℕ × ℕ
hcn : c.1 + c.2 = n
hc : (PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • (x ^ n).coeff g ≠ 0
⊢ ((PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • x ^ (c.1 + c.2)).coeff g ≠ 0
Module: Mathlib.RingTheory.HahnSeries.Binomial

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
h✝ : Nontrivial A
⊢ 0 < ((binomialFamily x r).hsum - 1).orderTop

Tactic:
refine (orderTop_self_sub_one_pos_iff (binomialFamily x r).hsum).mpr ?_

Goal state after:
case inr
Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
h✝ : Nontrivial A
⊢ (binomialFamily x r).hsum.orderTop = 0 ∧ (binomialFamily x r).hsum.leadingCoeff = 1
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
f : R →+* S
⊢ subst ![subst ![X 0, X 1] ((MvPowerSeries.map f) F.toPowerSeries), X 2] ((MvPowerSeries.map f) F.toPowerSeries) =
    subst ![X 0, subst ![X 1, X 2] ((MvPowerSeries.map f) F.toPowerSeries)] ((MvPowerSeries.map f) F.toPowerSeries)

Tactic:
by
    have (g₁ g₂ : MvPowerSeries (Fin 3) R) : ![g₁.map f, g₂.map f] =
      fun i => (![g₁, g₂] i).map f := by ext1 i; fin_cases i <;> simp
    simp_rw [(map_X f _).symm, this, ← map_subst .X_X, this, ← map_subst
      (HasSubst.cons_subst_zero_left (0 : Fin 3) 1 2 F.zero_constantCoeff), F.assoc,
      ← map_subst (HasSubst.cons_subst_zero_right (0 : Fin 3) 1 2 F.zero_constantCoeff)]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
⊢ (heval x) X = x

Tactic:
rw [X_eq, monomial_eq_mk, heval_apply, powerSeriesFamily, smulFamily]
  simp only [coeff_mk, powers_toFun, hx, ↓reduceIte, ite_smul, one_smul, zero_smul]
  ext g
  rw [coeff_hsum, finsum_eq_single _ 1 (fun n hn ↦ by simp [hn])]
  simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
g : Γ
⊢ {a | ¬(0 ^ a).coeff g = 0} ⊆ {0}

Tactic:
simp only [Set.subset_singleton_iff, Set.mem_ofPred_eq]
  intro n hn
  by_contra h'
  simp_all only [ne_eq, not_false_eq_true, zero_pow, coeff_zero, not_true_eq_false]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
m : ℕ
e : Bool
s : ℕ
⊢ (single 0) (OfScientific.ofScientific m e s) = OfScientific.ofScientific m e s

Tactic:
by
  simpa using single_zero_ratCast (Γ := Γ) (R := R) (OfScientific.ofScientific m e s)

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m n : ℕ
hmn : m ≤ n
⊢ c m ≡ c n [SMOD I ^ m • 1]

Tactic:
Ideal.smul_eq_mul,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m n : ℕ
hmn : m ≤ n
⊢ c m ≡ c n [SMOD I ^ m * 1]
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
⊢ ∃ a, f.IsRoot a ∧ a - a₀ ∈ I

Tactic:
obtain ⟨a, ha⟩ := IsPrecomplete.prec' c (aux _ _)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : ∀ (n : ℕ), c n ≡ a [SMOD I ^ n • ⊤]
⊢ ∃ a, f.IsRoot a ∧ a - a₀ ∈ I
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
n : ℕ
ha : c n ≡ a [SMOD I ^ n • 1]
⊢ Polynomial.eval a f ≡ 0 [SMOD I ^ n • 1]

Tactic:
Ideal.smul_eq_mul,

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
n : ℕ
ha : c n ≡ a [SMOD I ^ n * 1]
⊢ Polynomial.eval a f ≡ 0 [SMOD I ^ n * 1]
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : c 0 - Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ ≡ a [SMOD I • 1]
⊢ a - a₀ ∈ I

Tactic:
Ideal.smul_eq_mul,

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : c 0 - Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ ≡ a [SMOD I * 1]
⊢ a - a₀ ∈ I
Module: Mathlib.RingTheory.IdealFilter.Topology

Goal state before:
pp: case mpr
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
⊢ (∃ I ∈ F, a +ᵥ idealSet I ⊆ s) → s ∈ 𝓝 a

Tactic:
rintro ⟨I, hI, hIs⟩
    refine ((F.addGroupFilterBasis).nhds_hasBasis a).mem_iff.2 ?_
    exact ⟨I, ⟨I, hI, rfl⟩, hIs⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
this✝ : p.IsPrime
hp : maximalIdeal (Localization p.primeCompl) ∈ (span (⇑(algebraMap R (Localization p.primeCompl)) '' ↑s)).minimalPrimes
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
hn : s.card ≤ n + 1
this :
  ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
    p ∈ (span ↑s).minimalPrimes →
      p.IsPrime →
        ∀ (n : ℕ),
          (∀ m < n + 1,
              ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
                p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m) →
            s.card ≤ n + 1 → (∃ (x : IsLocalRing R), p = maximalIdeal R) → p.height ≤ ↑(n + 1)
hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R
⊢ maximalIdeal (Localization p.primeCompl) ∈
    (span ↑(Finset.image (⇑(algebraMap R (Localization p.primeCompl))) s)).minimalPrimes

Tactic:
by simpa using hp

Goal state after: