mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: 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 : q.height = 0
⊢ q.height < ↑1

Tactic:
rw [this]

Goal state after:
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 : q.height = 0
⊢ 0 < ↑1
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a (derivative f))
c : R
h✝ :
  c * (b - a) ^ 2 + Polynomial.eval a (derivative f) * (b - a) + Polynomial.eval a f = Polynomial.eval (a + (b - a)) f
hc : (c * (b - a) + Polynomial.eval a (derivative f)) * (b - a) = 0
this : c * (b - a) + Polynomial.eval a (derivative f) ∉ maximalIdeal R
⊢ a = b

Tactic:
rw [notMem_maximalIdeal, isUnit_iff_exists] at this

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a (derivative f))
c : R
h✝ :
  c * (b - a) ^ 2 + Polynomial.eval a (derivative f) * (b - a) + Polynomial.eval a f = Polynomial.eval (a + (b - a)) f
hc : (c * (b - a) + Polynomial.eval a (derivative f)) * (b - a) = 0
this :
  ∃ b_1,
    (c * (b - a) + Polynomial.eval a (derivative f)) * b_1 = 1 ∧
      b_1 * (c * (b - a) + Polynomial.eval a (derivative f)) = 1
⊢ a = b
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
I : Ideal A
x : A
hx : x ∈ I
J : Ideal A
hJ : J ∈ ↑F
⊢ ⊤ = Submodule.colon I {x}

Tactic:
by simpa [eq_comm]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
f : ↥J ⧸ I • ⊤ →ₗ[R] R ⧸ I := (I • ⊤).mapQ I (Submodule.subtype J) ⋯
this :
  LinearMap.lTensor (R ⧸ I) (Submodule.subtype J) =
    ↑(TensorProduct.rid R (R ⧸ I)).symm ∘ₗ f ∘ₗ ↑(quotTensorEquivQuotSMul (↥J) I)
⊢ Function.Injective ⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) ↔ I ⊓ J = I * J

Tactic:
rw [this]

Goal state after:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
f : ↥J ⧸ I • ⊤ →ₗ[R] R ⧸ I := (I • ⊤).mapQ I (Submodule.subtype J) ⋯
this :
  LinearMap.lTensor (R ⧸ I) (Submodule.subtype J) =
    ↑(TensorProduct.rid R (R ⧸ I)).symm ∘ₗ f ∘ₗ ↑(quotTensorEquivQuotSMul (↥J) I)
⊢ Function.Injective ⇑(↑(TensorProduct.rid R (R ⧸ I)).symm ∘ₗ f ∘ₗ ↑(quotTensorEquivQuotSMul (↥J) I)) ↔ I ⊓ J = I * J
Module: Mathlib.RingTheory.Ideal.Pure

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I J : Ideal R
inst✝ : I.Pure
⊢ Function.Injective ⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J))

Tactic:
apply Module.Flat.lTensor_preserves_injective_linearMap

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I J : Ideal R
inst✝ : I.Pure
⊢ Function.Injective ⇑(Submodule.subtype J)
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
s : Finset R
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
w✝ : IsLocalRing R
hp : maximalIdeal R ∈ (span ↑s).minimalPrimes
this : (maximalIdeal R).IsPrime
⊢ ∀ (q : Ideal R),
    q.IsPrime → q < maximalIdeal R → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R) → q.height ≤ ↑n

Tactic:
intro q

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
s : Finset R
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
w✝ : IsLocalRing R
hp : maximalIdeal R ∈ (span ↑s).minimalPrimes
this : (maximalIdeal R).IsPrime
q : Ideal R
⊢ q.IsPrime → q < maximalIdeal R → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R) → q.height ≤ ↑n
Module: Mathlib.RingTheory.KrullDimension.Module

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ supportDim R M = ⊥ ↔ Subsingleton M

Tactic:
by
  simp [supportDim, krullDim_eq_bot_iff, support_eq_empty_iff]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : PrimeSpectrum R
⊢ ringKrullDim (p.asIdeal.Fiber R[X]) ≤ ↑1

Tactic:
← ringKrullDim_eq_of_ringEquiv (polyEquivTensor R (p.asIdeal.ResidueField)).toRingEquiv,

Goal state after:
R : Type u_1
inst✝ : CommRing R
p : PrimeSpectrum R
⊢ ringKrullDim p.asIdeal.ResidueField[X] ≤ ↑1
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : n = 0
⊢ 1 = Fin.last p.length

Tactic:
Fin.last,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : n = 0
⊢ 1 = ⟨p.length, ⋯⟩
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h✝ : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
x : M
hx : x ∈ N
y : M
x✝ : x + a ^ n • y ∈ f n ⊓ (N + a ^ n • ⊤)
h1 : x + a ^ n • y ∈ ↑(f n)
h : (a ^ n • y ∈ N) = (a ^ (n + n) • y ∈ N)
⊢ x + a ^ n • y ∈ N

Tactic:
pow_add,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h✝ : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
x : M
hx : x ∈ N
y : M
x✝ : x + a ^ n • y ∈ f n ⊓ (N + a ^ n • ⊤)
h1 : x + a ^ n • y ∈ ↑(f n)
h : (a ^ n • y ∈ N) = ((a ^ n * a ^ n) • y ∈ N)
⊢ x + a ^ n • y ∈ N
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro
D : Type u_1
inst✝² : Finite D
inst✝¹ : Ring D
inst✝ : IsDomain D
val✝ : Fintype D
⊢ IsField D

Tactic:
let _ := Fintype.divisionRingOfIsDomain D

Goal state after:
case intro
D : Type u_1
inst✝² : Finite D
inst✝¹ : Ring D
inst✝ : IsDomain D
val✝ : Fintype D
x✝ : DivisionRing D := divisionRingOfIsDomain D
⊢ IsField D
Module: Mathlib.RingTheory.Invariant.Profinite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u
inst✝¹⁰ : Group G
inst✝⁹ : MulSemiringAction G B
inst✝⁸ : SMulCommClass G A B
inst✝⁷ : TopologicalSpace G
inst✝⁶ : CompactSpace G
inst✝⁵ : TotallyDisconnectedSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : TopologicalSpace B
inst✝² : DiscreteTopology B
inst✝¹ : ContinuousSMul G B
inst✝ : IsInvariant A B G
x : B
N : OpenNormalSubgroup G
hN : ↑N ⊆ ↑(MulAction.stabilizer G x)
this : IsIntegral A ⟨x, ⋯⟩
⊢ IsIntegral A x

Tactic:
exact this.map (FixedPoints.subalgebra A B N.1.1).val

Goal state after:
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalIso R S
inst✝ : IsLocalIso S T
s : Set S := {g | IsStandardOpenImmersion R (Localization.Away g)}
T' : S → Type u_3 := fun g ↦ Localization.Away ((algebraMap S T) g)
this✝³ : (g : S) → Algebra (Localization.Away g) (T' g) := fun g ↦ localizationAlgebra (Submonoid.powers g) T
T'' : S → T → Type u_3 := fun g x ↦ Localization.Away ((algebraMap T (T' g)) x)
t : S → Set T := fun g ↦ {x | IsStandardOpenImmersion (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : ↑s) × ↑(t ↑i)
this✝² : ∀ (i : ι), IsStandardOpenImmersion (Localization.Away ↑i.fst) (T'' ↑i.fst ↑i.snd)
h1 : Ideal.span (⇑(algebraMap S T) '' {g | IsStandardOpenImmersion R (Localization.Away g)}) = ⊤
g : S
hg : IsStandardOpenImmersion R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion S (Localization.Away x)
this✝¹ : Algebra (Localization.Away x) (T'' g x) := localizationAlgebra (Submonoid.powers x) (T' g)
this✝ : IsScalarTower S (Localization.Away x) (T'' g x)
this :
  algebraMapSubmonoid (Localization.Away x) (Submonoid.powers g) =
    algebraMapSubmonoid (Localization.Away x) (Submonoid.powers ((algebraMap S T) g))
⊢ IsLocalization (algebraMapSubmonoid (Localization.Away x) (Submonoid.powers g)) (T'' g x)

Tactic:
rw [this]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalIso R S
inst✝ : IsLocalIso S T
s : Set S := {g | IsStandardOpenImmersion R (Localization.Away g)}
T' : S → Type u_3 := fun g ↦ Localization.Away ((algebraMap S T) g)
this✝³ : (g : S) → Algebra (Localization.Away g) (T' g) := fun g ↦ localizationAlgebra (Submonoid.powers g) T
T'' : S → T → Type u_3 := fun g x ↦ Localization.Away ((algebraMap T (T' g)) x)
t : S → Set T := fun g ↦ {x | IsStandardOpenImmersion (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : ↑s) × ↑(t ↑i)
this✝² : ∀ (i : ι), IsStandardOpenImmersion (Localization.Away ↑i.fst) (T'' ↑i.fst ↑i.snd)
h1 : Ideal.span (⇑(algebraMap S T) '' {g | IsStandardOpenImmersion R (Localization.Away g)}) = ⊤
g : S
hg : IsStandardOpenImmersion R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion S (Localization.Away x)
this✝¹ : Algebra (Localization.Away x) (T'' g x) := localizationAlgebra (Submonoid.powers x) (T' g)
this✝ : IsScalarTower S (Localization.Away x) (T'' g x)
this :
  algebraMapSubmonoid (Localization.Away x) (Submonoid.powers g) =
    algebraMapSubmonoid (Localization.Away x) (Submonoid.powers ((algebraMap S T) g))
⊢ IsLocalization (algebraMapSubmonoid (Localization.Away x) (Submonoid.powers ((algebraMap S T) g))) (T'' g x)
Module: Mathlib.RingTheory.Invariant.Profinite

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
B' : (G : Type u) → [inst : Monoid G] → [inst_1 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
s : (j : OpenNormalSubgroup G) → (stabilizerHomSurjectiveAuxFunctor P Q σ).obj j
hs : s ∈ (stabilizerHomSurjectiveAuxFunctor P Q σ).sections
a : ↑(ProfiniteGrp.of G).toProfinite.toTop :=
  (ProfiniteGrp.Hom.hom (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor.inv) ⟨fun N ↦ ↑↑(s N), ⋯⟩
this : ∀ (N : OpenNormalSubgroup G), ↑a = ↑↑(s N)
N : OpenNormalSubgroup G
x : ↥(B' ↥↑N.toOpenSubgroup)
hN : ↑N ⊆ ↑(MulAction.stabilizer G ↑x)
⊢ (mk Q) ↑(↑a • x) = σ ((mk Q) ↑x)

Tactic:
rw [this]

Goal state after:
case refine_2
A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
B' : (G : Type u) → [inst : Monoid G] → [inst_1 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
s : (j : OpenNormalSubgroup G) → (stabilizerHomSurjectiveAuxFunctor P Q σ).obj j
hs : s ∈ (stabilizerHomSurjectiveAuxFunctor P Q σ).sections
a : ↑(ProfiniteGrp.of G).toProfinite.toTop :=
  (ProfiniteGrp.Hom.hom (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor.inv) ⟨fun N ↦ ↑↑(s N), ⋯⟩
this : ∀ (N : OpenNormalSubgroup G), ↑a = ↑↑(s N)
N : OpenNormalSubgroup G
x : ↥(B' ↥↑N.toOpenSubgroup)
hN : ↑N ⊆ ↑(MulAction.stabilizer G ↑x)
⊢ (mk Q) ↑(↑↑(s N) • x) = σ ((mk Q) ↑x)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 ≤ HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ

Tactic:
obtain ⟨P, hP⟩ := exists_Polynomial_intValuation_lt (PowerSeries.X ^ s * F) γ

Goal state after:
case neg
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 ≤ HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
P : K[X]
hP : (PowerSeries.idealX K).intValuation (PowerSeries.X ^ s * F - ↑P) < ↑γ
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 ≤ HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
P : K[X]
hP : (PowerSeries.idealX K).intValuation (PowerSeries.X ^ s * F - ↑P) < ↑γ
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ

Tactic:
use P

Goal state after:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := ⋯
hF : F = f.powerSeriesPart
ord_nonpos : 0 ≤ HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
P : K[X]
hP : (PowerSeries.idealX K).intValuation (PowerSeries.X ^ s * F - ↑P) < ↑γ
⊢ Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) ↑P) < ↑γ
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SetRel.IsSymm V
T : Set K⸨X⸩
hT₀ : T ∈ nhds 0
hT₁ : (fun x ↦ -x.2 + x.1) ⁻¹' T ⊆ V
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hγ : {x | Valued.v.restrict x < ↑γ} ⊆ T
this : WithZero (Multiplicative ℤ)
P : K⟮X⟯
hP : Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) P) < ↑((Units.map ↑embedding) γ)
⊢ ∃ a, (algebraMap K⟮X⟯ K⸨X⸩) a ∈ UniformSpace.ball f V

Tactic:
use P

Goal state after:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SetRel.IsSymm V
T : Set K⸨X⸩
hT₀ : T ∈ nhds 0
hT₁ : (fun x ↦ -x.2 + x.1) ⁻¹' T ⊆ V
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hγ : {x | Valued.v.restrict x < ↑γ} ⊆ T
this : WithZero (Multiplicative ℤ)
P : K⟮X⟯
hP : Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) P) < ↑((Units.map ↑embedding) γ)
⊢ (algebraMap K⟮X⟯ K⸨X⸩) P ∈ UniformSpace.ball f V
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : t ∈ pairs σ k
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) + weight σ R k (pairMap σ t) = 0

Tactic:
weight

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : t ∈ pairs σ k
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(pairMap σ t).1 * ((∏ a ∈ (pairMap σ t).1, X a) * X (pairMap σ t).2 ^ (k - #(pairMap σ t).1)) =
    0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
n : ℕ
⊢ -1 * (-1) ^ n = (-1) ^ (n + 1)

Tactic:
pow_add,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
n : ℕ
⊢ -1 * (-1) ^ n = (-1) ^ n * (-1) ^ 1
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝¹⁰ : Ring R
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module (Matrix ι ι R) M
inst✝⁵ : Module R M
inst✝⁴ : IsScalarTower R (Matrix ι ι R) M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module (Matrix ι ι R) N
i : ι
inst✝¹ : Module R N
inst✝ : IsScalarTower R (Matrix ι ι R) N
f : M →ₗ[Matrix ι ι R] N
x : M
hx : x ∈ toModuleCatObj R M i
⊢ (↑R f) x ∈ toModuleCatObj R N i

Tactic:
obtain ⟨y, rfl⟩ := mem_toModuleCatObj i |>.1 hx
    exact ⟨f y, map_smul _ _ _ |>.symm⟩

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

Goal state before:
pp: case neg.a
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd₁ : (coeff d) φ ≠ 0
hd₂ : ↑(Finsupp.degree d) = φ.order
this : p • φ.order = ↑(Finsupp.degree (p • d))
⊢ ((expand p hp) φ).order ≤ p • φ.order

Tactic:
rw [this]

Goal state after:
case neg.a
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd₁ : (coeff d) φ ≠ 0
hd₂ : ↑(Finsupp.degree d) = φ.order
this : p • φ.order = ↑(Finsupp.degree (p • d))
⊢ ((expand p hp) φ).order ≤ ↑(Finsupp.degree (p • d))
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h.left
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : a = 0
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
⊢ {t | Valued.v t < γ} ∈ 𝓝 a

Tactic:
rw [ha, this]
      obtain ⟨x, hx⟩ := valuedAdicCompletion_surjective K⟮X⟯ (idealX K) γ
      use Units.mk0 (Valued.v.restrict x) (by
        simp only [Valuation.restrict_def, ne_eq, map_eq_zero]
        intro h
        simp only [h, map_zero] at hx
        tauto)
      simp [Units.val_mk0, Valuation.restrict_lt_iff, hx]

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

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
i : σ
hi : ¬p ∣ d i
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) = 0

Tactic:
by_cases hd : d ≤ p • n

Goal state after:
case pos
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
i : σ
hi : ¬p ∣ d i
hd : d ≤ p • n
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) = 0

case neg
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
i : σ
hi : ¬p ∣ d i
hd : ¬d ≤ p • n
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) = 0
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
key :
  (expand p) ((bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)) =
    (expand p) ((bind₁ (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n))
⊢ (bind₁ fun i ↦ (expand p) ((rename fun i_1 ↦ (i, i_1)) (W_ ℚ n))) ((map (Int.castRingHom ℚ)) Φ) =
    (bind₁ fun i ↦ (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)

Tactic:
simp only [expand_bind₁] at key

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
key :
  (bind₁ fun i ↦ (expand p) ((rename (Prod.mk i)) (W_ ℚ n))) ((map (Int.castRingHom ℚ)) Φ) =
    (bind₁ fun i ↦ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n)
⊢ (bind₁ fun i ↦ (expand p) ((rename fun i_1 ↦ (i, i_1)) (W_ ℚ n))) ((map (Int.castRingHom ℚ)) Φ) =
    (bind₁ fun i ↦ (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, ↑p ∣ x.coeff i
i : ℕ
hi : i < n + 1
this : (aeval x.coeff) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i)) = ↑p ^ i * x.coeff i ^ p ^ (n - i)
⊢ ↑p ^ (n - i + 1 + i) ∣ ↑p ^ i * x.coeff i ^ p ^ (n - i)

Tactic:
pow_add,

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, ↑p ∣ x.coeff i
i : ℕ
hi : i < n + 1
this : (aeval x.coeff) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i)) = ↑p ^ i * x.coeff i ^ p ^ (n - i)
⊢ ↑p ^ (n - i + 1) * ↑p ^ i ∣ ↑p ^ i * x.coeff i ^ p ^ (n - i)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑(p ^ (n + 1)) ∣
    ↑(p ^ k) * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))

Tactic:
rw [this]

Goal state after:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑(p ^ k * p ^ (n - k + 1)) ∣
    ↑(p ^ k) * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
m n✝ n : ℕ
ih : (coeffMonoidHom M p (m + n)) (f ^ p ^ n) = (coeffMonoidHom M p m) f
⊢ (coeffMonoidHom M p (m + n).succ) ((f ^ p ^ n) ^ p) = (coeffMonoidHom M p m) f

Tactic:
coeffMonoidHom_pow_p,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
m n✝ n : ℕ
ih : (coeffMonoidHom M p (m + n)) (f ^ p ^ n) = (coeffMonoidHom M p m) f
⊢ (coeffMonoidHom M p (m + n)) (f ^ p ^ n) = (coeffMonoidHom M p m) f
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: case refine_1
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ liftFun f 1 = 1

Tactic:
( intros
    rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]
    simp [RingHom.mem_ker, f_compat])

Goal state after: