mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf : ∀ (i : Fin n), (f (MvPolynomial.X i)).degrees ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
hg : g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) = ↑f
σ : MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) (MvPolynomial (Fin n) R) :=
  MvPolynomial.map (algebraMap R (MvPolynomial (Fin n) R))
hσ : g.comp σ = RingHom.id (MvPolynomial (Fin m) R)
hσ' : ∀ (x : MvPolynomial (Fin m) R), g (σ x) = x
hg' : Surjective ⇑g
S' : ConstructibleSetData (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Finset.image
    (fun x ↦
      match x with
      | { f := fk, n := k, g := gk } =>
        { f := σ fk, n := k + n,
          g := fun s ↦
            Sum.elim (⇑σ ∘ gk) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i)))
              (finSumFinEquiv.symm s) })
    S
s₀ : Set (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Set.range fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))
H : Ideal.span s₀ ≤ RingHom.ker g
q₁ : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)
q₂ : MvPolynomial (Fin m) R
hq₁ : q₁ ∈ Ideal.span s₀
hp : q₁ + σ q₂ ∈ RingHom.ker g
⊢ q₂ = 0

Tactic:
simpa [hσ', show g q₁ = 0 from H hq₁] using hp

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case right.inl
R : Type u_2
inst✝ : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf : ∀ (i : Fin n), (f (MvPolynomial.X i)).degrees ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
hg : g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) = ↑f
σ : MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) (MvPolynomial (Fin n) R) :=
  MvPolynomial.map (algebraMap R (MvPolynomial (Fin n) R))
hσ : g.comp σ = RingHom.id (MvPolynomial (Fin m) R)
hσ' : ∀ (x : MvPolynomial (Fin m) R), g (σ x) = x
hg' : Surjective ⇑g
S' : ConstructibleSetData (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Finset.image
    (fun x ↦
      match x with
      | { f := fk, n := k, g := gk } =>
        { f := σ fk, n := k + n,
          g := fun s ↦
            Sum.elim (⇑σ ∘ gk) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i)))
              (finSumFinEquiv.symm s) })
    S
s₀ : Set (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Set.range fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))
hs : zeroLocus s₀ = Set.range (comap g)
hg'' : ∀ (t : Set (PrimeSpectrum (MvPolynomial (Fin m) R))), comap g '' t = comap σ ⁻¹' t ∩ zeroLocus s₀
hS' : comap g '' S.toSet = S'.toSet
x : BasicConstructibleSetData (MvPolynomial (Fin m) R)
hx : x ∈ S
j : Fin x.n
⊢ (Sum.elim (⇑σ ∘ x.g) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))) (Sum.inl j)).degrees ≤ d

Tactic:
simp only [MvPolynomial.algebraMap_eq, Sum.elim_inl, comp_apply, σ]
          exact degrees_map_le.trans (hS _ hx j)

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case mp
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
P : W.Point
⊢ toClass P = 0 → P = 0

pp: case mpr
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
P : W.Point
⊢ P = 0 → toClass P = 0

Tactic:
· intro hP
    rcases P with (_ | ⟨_, _, h, _⟩)
    · rfl
    · rcases (ClassGroup.mk_eq_one_of_coe_ideal <| by rfl).mp hP with ⟨p, h0, hp⟩
      apply (p.natDegree_norm_ne_one _).elim
      rw [← finrank_quotient_span_eq_natDegree_norm (CoordinateRing.basis W) h0,
        ← (quotientEquivAlgOfEq F hp).toLinearEquiv.finrank_eq,
        (CoordinateRing.quotientXYIdealEquiv h).toLinearEquiv.finrank_eq, Module.finrank_self]

Goal state after:
case mpr
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
P : W.Point
⊢ P = 0 → toClass P = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C X * (C W.preΨ₄ * W.ψ₂) ^ 2 - (C W.preΨ₄ * W.ψ₂ * W.ψ₂ ^ 3 - 1 * W.ψ (2 + 1) ^ 3) * W.ψ (4 - 1) =
    C X * C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 4 * C W.Ψ₃ + C W.Ψ₃ ^ 4

Tactic:
two_add_one_eq_three,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C X * (C W.preΨ₄ * W.ψ₂) ^ 2 - (C W.preΨ₄ * W.ψ₂ * W.ψ₂ ^ 3 - 1 * W.ψ 3 ^ 3) * W.ψ (4 - 1) =
    C X * C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 4 * C W.Ψ₃ + C W.Ψ₃ ^ 4
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ (W⁄B).Φ n = Polynomial.map (↑f) ((W⁄A).Φ n)

Tactic:
by
  rw [← map_Φ, map_baseChange]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: case a₄
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
⊢ W.a₁ * (W.a₁ * W.a₄ + 2 * W.a₃ * W.a₂) - (W.a₁ ^ 2 * W.a₄ + W.a₃ ^ 2) + W.a₃ ^ 2 * 3 = 0

Tactic:
linear_combination (W.a₃ ^ 2 + W.a₁ * W.a₃ * W.a₂) * CharP.cast_eq_zero F 2

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4) = 0 ∧
    2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3 = 0 ∧
      W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 -
          (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5) =
        0
⊢ W'.a₁ * (u ^ 2 * P x) * (u ^ 3 * P y) + 3 * W'.a₃ * (u ^ 3 * P y) * (u * P z) ^ 2 -
      (2 * W'.a₂ * (u ^ 2 * P x) ^ 2 * (u * P z) + 4 * W'.a₄ * (u ^ 2 * P x) * (u * P z) ^ 3 +
        6 * W'.a₆ * (u * P z) ^ 5) =
    0

Tactic:
linear_combination (norm := ring1) u ^ 5 * hP'.right.right

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ {u : R}, IsUnit u → ∀ {P : Fin 3 → R}, W'.Nonsingular (u • P) → W'.Nonsingular P
h : W'.Nonsingular P
⊢ W'.Nonsingular (↑hu.unit⁻¹ • u • P)

Tactic:
by rwa [smul_smul, hu.val_inv_mul, one_smul]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
P : Fin 3 → A
⊢ (W'⁄B).Nonsingular (⇑↑f ∘ P) ↔ (W'⁄A).Nonsingular P

Tactic:
← map_nonsingular _ hf,

Goal state after:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
P : Fin 3 → A
⊢ (W'⁄B).Nonsingular (⇑↑f ∘ P) ↔ ((W'⁄A).map f.toRingHom).Nonsingular (⇑f.toRingHom ∘ P)
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: case neg.e_a.e_6
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(unzero hxy) = ↑(unzero hx * unzero hy)

Tactic:
WithZero.coe_mul,

Goal state after:
case neg.e_a.e_6
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(unzero hxy) = ↑(unzero hx) * ↑(unzero hy)
Module: Mathlib.RingTheory.Valuation.ExtendToLocalization

Goal state before:
pp: case h.left
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : S.LocalizationMap B := ⋯
h : ∀ (s : ↥S), IsUnit (↑v.toMonoidWithZeroHom ↑s) := ⋯
a : A
s : ↥S
b : A
t : ↥S
⊢ f.mk' (a * ↑t) (s * t) = f.mk' a s

Tactic:
rw [f.mk'_eq_iff_eq, Submonoid.coe_mul]
            ring_nf

Goal state after:
Module: Mathlib.RingTheory.Valuation.ExtendToLocalization

Goal state before:
pp: case h.right
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : S.LocalizationMap B := ⋯
h : ∀ (s : ↥S), IsUnit (↑v.toMonoidWithZeroHom ↑s) := ⋯
a : A
s : ↥S
b : A
t : ↥S
⊢ f.mk' (b * ↑s) (s * t) = f.mk' b t

Tactic:
rw [f.mk'_eq_iff_eq, Submonoid.coe_mul]
            ring_nf

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := ⋯
⊢ ∀ U ∈ 𝓝 0, ∃ V, ↑V ⊆ U

Tactic:
intro U hU

Goal state after:
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := hB.topology
U : Set A
hU : U ∈ 𝓝 0
⊢ ∃ V, ↑V ⊆ U
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
this : TopologicalSpace M := ⋯
⊢ ∀ U ∈ 𝓝 0, ∃ V, ↑V ⊆ U

Tactic:
intro U hU

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
this : TopologicalSpace M := hB.topology
U : Set M
hU : U ∈ 𝓝 0
⊢ ∃ V, ↑V ⊆ U
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ Tendsto f l (𝓝 γ) ↔ ∀ᶠ (x : α) in l, f x = γ

Tactic:
nhds_of_ne_zero h,

Goal state after:
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ Tendsto f l (pure γ) ↔ ∀ᶠ (x : α) in l, f x = γ
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: case pos
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure[topologicalSpace] s) t
h₂ : Disjoint s (closure[topologicalSpace] t)
hs : 0 ∈ s
ht : 0 ∉ t
⊢ Disjoint (𝓝ˢ s) (𝓟 t)

Tactic:
disjoint_nhdsSet_principal

Goal state after:
case pos
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure[topologicalSpace] s) t
h₂ : Disjoint s (closure[topologicalSpace] t)
hs : 0 ∈ s
ht : 0 ∉ t
⊢ Disjoint s (closure[topologicalSpace] t)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
c : ValueGroupWithZero R
a₁ : R
a₂ : ↥(posSubmonoid R)
b₁ : R
b₂ : ↥(posSubmonoid R)
hbc : ValueGroupWithZero.mk b₁ b₂ ≤ c
hab : ValueGroupWithZero.mk a₁ a₂ ≤ ValueGroupWithZero.mk b₁ b₂
⊢ ValueGroupWithZero.mk a₁ a₂ ≤ c

Tactic:
| mk b₁ b₂
     => 

Goal state after:
case mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
c : ValueGroupWithZero R
a₁ : R
a₂ : ↥(posSubmonoid R)
b₁ : R
b₂ : ↥(posSubmonoid R)
hbc : ValueGroupWithZero.mk b₁ b₂ ≤ c
hab : ValueGroupWithZero.mk a₁ a₂ ≤ ValueGroupWithZero.mk b₁ b₂
⊢ ValueGroupWithZero.mk a₁ a₂ ≤ c
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z x✝¹ : R
y✝¹ : ↥(posSubmonoid R)
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x✝¹ y✝¹ ≤ ValueGroupWithZero.mk x✝ y✝ ∨
    ValueGroupWithZero.mk x✝ y✝ ≤ ValueGroupWithZero.mk x✝¹ y✝¹

Tactic:
rw [ValueGroupWithZero.mk_le_mk, ValueGroupWithZero.mk_le_mk]

Goal state after:
case mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z x✝¹ : R
y✝¹ : ↥(posSubmonoid R)
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ x✝¹ * ↑y✝ ≤ᵥ x✝ * ↑y✝¹ ∨ x✝ * ↑y✝¹ ≤ᵥ x✝¹ * ↑y✝
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : TopologicalSpace R
v : Valuation R Γ₀
inst✝ : v.Compatible
H : ∀ {s : Set R} {x : R}, s ∈ 𝓝 x ↔ ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s
⊢ IsValuativeTopology R

Tactic:
by
  constructor
  refine fun {s x} ↦ ⟨fun h_mem ↦ ?_, fun ⟨γ, hγ⟩ ↦
    H.mpr ⟨.mk0 ((orderMonoidIso v) γ) (by simp), subset_trans (by simp [neg_add_eq_sub]) hγ⟩⟩
  obtain ⟨γ, hγ⟩ := H.mp h_mem
  exact ⟨.mk0 ((orderMonoidIso v).symm γ) (by simp), subset_trans (by simp [neg_add_eq_sub]) hγ⟩

Goal state after:
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x ↦ x * x.hatInv
c : K → hat K := fun x ↦ ↑x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' c '' {0}ᶜ)
z : K
z_ne : z ≠ 0
⊢ (fun x ↦ f (c x)) z = 1

Tactic:
dsimp [f]

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x ↦ x * x.hatInv
c : K → hat K := fun x ↦ ↑x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' c '' {0}ᶜ)
z : K
z_ne : z ≠ 0
⊢ c z * (c z).hatInv = 1
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
⊢ CompletableTopField α

Tactic:
refine CompletableTopField.mk (fun F F_cau inf_F => ?_)

Goal state after:
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy F
inf_F : 𝓝 0 ⊓ F = ⊥
⊢ Cauchy (map (fun x ↦ x⁻¹) F)
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case hH.negSucc.refine_1
A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n✝ : (WithZero (Multiplicative ℤ))ˣ
hπ✝ : (exp 1)⁻¹ ∈ range ⇑v
x✝ : ∃ k, Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n✝
π : A
hπ : v π = (exp 1)⁻¹
n : ℕ
h : Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.negSucc n = n✝
⊢ ¬(MonoidWithZeroHom.ofClass v) (π ^ (n + 1)) = 0

Tactic:
simp [hπ, Int.negSucc_eq, mul_assoc]

Goal state after:
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case hH.negSucc.refine_2
A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n✝ : (WithZero (Multiplicative ℤ))ˣ
hπ✝ : (exp 1)⁻¹ ∈ range ⇑v
x✝ : ∃ k, Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n✝
π : A
hπ : v π = (exp 1)⁻¹
n : ℕ
h : Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.negSucc n = n✝
⊢ (MonoidWithZeroHom.ofClass v) (π ^ (n + 1)) * ↑(Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.negSucc n) =
    (MonoidWithZeroHom.ofClass v) 1

Tactic:
simp [hπ, Int.negSucc_eq, mul_assoc]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R✝ : Type u_1
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
⊢ ↑(ofClass Valued.v).valueGroup = ↑(ofClass v).valueGroup

Tactic:
simp [valueGroup_eq v]

Goal state after:
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝¹ : Field K
v : Valuation K Γ
inst✝ : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : maximalIdeal ↥v.valuationSubring = span {r}
hr₀ : r ≠ 0
π : ↥v.valuationSubring
hπ : v.IsUniformizer ↑π
⊢ v.IsUniformizer ↑r

Tactic:
obtain ⟨n, u, hu⟩ := exists_pow_Uniformizer hr₀ ⟨π, hπ⟩

Goal state after:
Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝¹ : Field K
v : Valuation K Γ
inst✝ : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : maximalIdeal ↥v.valuationSubring = span {r}
hr₀ : r ≠ 0
π : ↥v.valuationSubring
hπ : v.IsUniformizer ↑π
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : ↑r = ↑({ val := π, valuation_gt_one := hπ }.val ^ n) * ↑↑u
⊢ v.IsUniformizer ↑r
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero G
inst✝ : MulArchimedean G
a : G
ha : a < 1
b : Gˣ
⊢ ∃ n, a ^ n < ↑b

Tactic:
by
  rcases eq_or_ne a 0 with rfl | ha'
  · use 1
    simp
  · lift a to Gˣ using IsUnit.mk0 _ ha'
    simpa using! exists_pow_lt ha b

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Subsingleton R
⊢ Subsingleton R⟦X⟧

Tactic:
by
  simp only [subsingleton_iff, PowerSeries.ext_iff]
  subsingleton

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case neg.hnc
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
hxy : v xy = embedding a * embedding b
hx : v x = embedding a
hy : v y = embedding b
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ¬extensionValuation ↑xy = 0

Tactic:
· simp [extensionValuation_apply_coe, hxy, ← hx, ← hy, hx0, hy0]

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

Goal state before:
pp: case top
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff d) f = 0
⊢ ⊤ ≤ weightedOrder w f

Tactic:
top_le_iff,

Goal state after:
case top
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff d) f = 0
⊢ weightedOrder w f = ⊤
Module: Mathlib.Data.Finset.Finsupp

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
hi : i ∉ s
⊢ f i ∈ t i

Tactic:
· rw [notMem_support_iff.1 (mt h.1 hi), notMem_support_iff.1 fun H => hi <| ht H]
      exact zero_mem_zero

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

Goal state before:
pp: case left
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
⊢ ∃ d, (coeff d) (f + g) ≠ 0 ∧ (weight w) d = n

pp: case right
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
⊢ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) (f + g) = 0

Tactic:
· refine ⟨d, ?_, hd⟩
    rw [← hn, ← hd] at H
    rw [(coeff _).map_add, coeff_eq_zero_of_lt_weightedOrder w H, add_zero]
    exact hd'

Goal state after:
case right
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
⊢ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) (f + g) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
d : σ →₀ ℕ
hd : ¬(weight w) d = p
⊢ (coeff d) f = 0

Tactic:
· exact hf.coeff_eq_zero hd

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ Function.Surjective ⇑Valued.v

Tactic:
have h : Function.Surjective (Valued.v : (v.valuation K).Completion → ℤᵐ⁰) :=
    Valued.valuedCompletion_surjective_iff.mpr <| .of_comp (v.valuation_surjective K)

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
h : Function.Surjective ⇑Valued.v
⊢ Function.Surjective ⇑Valued.v
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
⊢ Tendsto (fun x ↦ X x) cofinite (𝓝 0)

Tactic:
classical
  simp only [tendsto_iff_coeff_tendsto, coeff_X, coeff_zero]
  refine fun d ↦ tendsto_nhds_of_eventually_eq ?_
  by_cases! h : ∃ i, d = Finsupp.single i 1
  · obtain ⟨i, hi⟩ := h
    filter_upwards [eventually_cofinite_ne i] with j hj
    simp [hi, Finsupp.single_eq_single_iff, hj.symm]
  · simpa only [ite_eq_right_iff] using
      Eventually.of_forall fun x h' ↦ (h x h').elim

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ.order ≤ MvPowerSeries.order φ

Tactic:
refine MvPowerSeries.le_order fun d hd => by
      have : coeff ↑(Finsupp.degree d) φ = 0 := coeff_of_lt_order _ hd
      have eq_aux : d.degree = d () := Finset.sum_eq_single _ (by simp) (by simp)
      exact (PowerSeries.coeff_def rfl (R := R)) ▸ (eq_aux ▸ this)

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j).1 + (i, j).2 = n
hi : φ.order ≤ ↑i
hj : ψ.order ≤ ↑j
⊢ ↑n = ↑(i + j)

Tactic:
hij

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j).1 + (i, j).2 = n
hi : φ.order ≤ ↑i
hj : ψ.order ≤ ↑j
⊢ ↑n = ↑n
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
ij : ℕ × ℕ
⊢ ij ∈ antidiagonal (φ.order.toNat + ψ.order.toNat) →
    ij ≠ (φ.order.toNat, ψ.order.toNat) → (coeff ij.1) φ * (coeff ij.2) ψ = 0

Tactic:
hij

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
ij : ℕ × ℕ
hij : ij ∈ antidiagonal (φ.order.toNat + ψ.order.toNat)
⊢ ij ≠ (φ.order.toNat, ψ.order.toNat) → (coeff ij.1) φ * (coeff ij.2) ψ = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg.inr.inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h✝ : φ ≠ 0 ∧ ψ ≠ 0
ij : ℕ × ℕ
hij : ij ∈ antidiagonal (φ.order.toNat + ψ.order.toNat)
h : ij ≠ (φ.order.toNat, ψ.order.toNat)
h' : ij.2 < ψ.order.toNat
⊢ (coeff ij.1) φ * (coeff ij.2) ψ = 0

Tactic:
rw [coeff_of_lt_order_toNat ij.2 h', mul_zero]

Goal state after: