mathlib-initiative/mathlib-tactics huggingface dataset:
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 ^ 3 * P y) * (u * P z) -
      (3 * (u ^ 2 * P x) ^ 2 + 2 * W'.a₂ * (u ^ 2 * P x) * (u * P z) ^ 2 + W'.a₄ * (u * P z) ^ 4) =
    0

Tactic:
by linear_combination (norm := ring1) u ^ 4 * hP'.left

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
a b : R
⊢ b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
        (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
      0 →
    W'.a₁ * b - (3 * a ^ 2 + 2 * W'.a₂ * a + W'.a₄) = 0 →
      (2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0 ↔
        2 * b + W'.a₁ * a + W'.a₃ = 0 ∧
          W'.a₁ * a * b + 3 * W'.a₃ * b - (2 * W'.a₂ * a ^ 2 + 4 * W'.a₄ * a + 6 * W'.a₆) = 0)

Tactic:
iff_self_and

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
a b : R
⊢ b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
        (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
      0 →
    W'.a₁ * b - (3 * a ^ 2 + 2 * W'.a₂ * a + W'.a₄) = 0 →
      2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0 →
        W'.a₁ * a * b + 3 * W'.a₃ * b - (2 * W'.a₂ * a ^ 2 + 4 * W'.a₄ * a + 6 * W'.a₆) = 0
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
f : R →+* S
⊢ (W'.map f).polynomial = (MvPolynomial.map f) W'.polynomial

Tactic:
simp only [polynomial]

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ «X» y ^ 2 + C (W'.map f).a₁ * «X» x * «X» y * «X» z + C (W'.map f).a₃ * «X» y * «X» z ^ 3 -
      («X» x ^ 3 + C (W'.map f).a₂ * «X» x ^ 2 * «X» z ^ 2 + C (W'.map f).a₄ * «X» x * «X» z ^ 4 +
        C (W'.map f).a₆ * «X» z ^ 6) =
    (MvPolynomial.map f)
      (Y ^ 2 + C W'.a₁ * X * Y * Z + C W'.a₃ * Y * Z ^ 3 -
        (X ^ 3 + C W'.a₂ * X ^ 2 * Z ^ 2 + C W'.a₄ * X * Z ^ 4 + C W'.a₆ * Z ^ 6))
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
⊢ (W'⁄B).polynomialX = (MvPolynomial.map ↑f) (W'⁄A).polynomialX

Tactic:
← map_polynomialX,

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
⊢ (W'⁄B).polynomialX = ((W'⁄A).map ↑f).polynomialX
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
S X✝ : Scheme
D✝ : I ⥤ Scheme
t : D✝ ⟶ (Functor.const I).obj S
f : X✝ ⟶ S
c✝ : Cone D✝
hc✝ : IsLimit c✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
⊢ Nonempty (IsColimit ((yoneda.obj X).mapCocone c))

Tactic:
by
    rw [Limits.Types.isColimit_iff_coconeTypesIsColimit]
    have (i : I) : CompactSpace ((D ⋙ Over.forget S).obj i) := by dsimp; infer_instance
    have (i : I) : QuasiSeparatedSpace ((D ⋙ Over.forget S).obj i) := by dsimp; infer_instance
    have {i j : I} (f : i ⟶ j) : IsAffineHom ((D ⋙ Over.forget S).map f) := by
      dsimp; infer_instance
    refine ⟨⟨?_, ?_⟩⟩
    · rw [Functor.CoconeTypes.descColimitType_injective_iff_of_isFiltered']
      intro k g₁ g₂ hg
      obtain ⟨k, hik, heq⟩ := Scheme.exists_hom_comp_eq_comp_of_locallyOfFiniteType
        (D ⋙ Over.forget _) (.mk (fun _ ↦ (D.obj _).hom)) X.hom _ (isLimitOfPreserves _ hc.unop)
        g₁.left g₂.left (Over.w g₁).symm (Over.w g₂).symm congr($(hg).left)
      use .op k, hik.op
      cat_disch
    · intro g
      obtain ⟨k, u, h, h'⟩ := Scheme.exists_π_app_comp_eq_of_locallyOfFinitePresentation
        (D ⋙ Over.forget _) (.mk (fun _ ↦ (D.obj _).hom)) X.hom _ (isLimitOfPreserves _ hc.unop)
        g.left (by ext; simp)
      use Functor.ιColimitType _ (.op k) (Over.homMk u)
      cat_disch

Goal state after:
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: case coe.zero
e : ℝ≥0
he : 1 < e
a✝ : Multiplicative ℤ
⊢ 0 < ↑a✝ → (toNNReal ⋯) 0 < (toNNReal ⋯) ↑a✝

Tactic:
simpa using! zpow_pos he.pos _

Goal state after:
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
⊢ (toNNReal he0) m = 1 ↔ m = 1

Tactic:
by_cases hm : m = 0
  · simp only [hm, map_zero, zero_ne_one]
  · refine ⟨fun h1 ↦ ?_, fun h1 ↦ h1 ▸ map_one _⟩
    rw [toNNReal_neg_apply he0 hm, zpow_eq_one_iff_right₀ _root_.zero_le he1, toAdd_eq_zero] at h1
    rw [← WithZero.coe_unzero hm, h1, coe_one]

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
inhabited_h : Inhabited ι
⊢ {U | ∃ i, U = ↑(B i)}.Nonempty

Tactic:
exact ⟨B default, default, rfl⟩

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
inhabited_h : Inhabited ι
⊢ {U | ∃ i, U = ↑(B i)}.Nonempty

Tactic:
exact ⟨B default, default, rfl⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
⊢ (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)

Tactic:
by_cases hw : w ≤ᵥ 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : w ≤ᵥ 0
⊢ (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)

case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : ¬w ≤ᵥ 0
⊢ (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
s : Set Γ₀
⊢ IsClosed[topologicalSpace] s ↔ 0 ∈ s ∨ ∃ γ, γ ≠ 0 ∧ s ⊆ Ici γ

Tactic:
simp only [← isOpen_compl_iff, isOpen_iff, mem_compl_iff, not_not, ← compl_Ici,
    compl_subset_compl]

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : TopologicalSpace R
inst✝ : IsValuativeTopology R
s : Set R
x : R
⊢ s ∈ 𝓝 x ↔ ∃ γ, {z | (valuation R) (z - x) < ↑γ} ⊆ s

Tactic:
convert! mem_nhds_iff (s := s) using 4

Goal state after:
case e'_2
R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : TopologicalSpace R
inst✝ : IsValuativeTopology R
s : Set R
x : R
x✝ : (ValueGroupWithZero R)ˣ
⊢ {z | (valuation R) (z - x) < ↑x✝} = (fun x_1 ↦ x + x_1) '' {z | (valuation R) z < ↑x✝}
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x : R
⊢ x ≤ᵥ 1 ↔ v x ≤ 1

Tactic:
by simp [v.vle_iff_le]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x : R
⊢ 1 ≤ᵥ x ↔ 1 ≤ v x

Tactic:
by simp [v.vle_iff_le]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
γ : ValueGroupWithZero R
hγ : γ ≠ 0
hγ' : γ ≠ 1
⊢ Nontrivial (ValueGroupWithZero R)ˣ

Tactic:
refine ⟨Units.mk0 _ hγ, 1, ?_⟩

Goal state after:
case mp
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
γ : ValueGroupWithZero R
hγ : γ ≠ 0
hγ' : γ ≠ 1
⊢ Units.mk0 γ hγ ≠ 1
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ IsOpen[_i.toTopologicalSpace] ↑v.integer

Tactic:
simp only [integer, Subring.coe_set_mk, Subsemiring.coe_set_mk, Submonoid.coe_set_mk,
    Subsemigroup.coe_set_mk, ← v.restrict_le_one_iff]

Goal state after:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ IsOpen[_i.toTopologicalSpace] {x | v.restrict x ≤ 1}
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ IsClosed[_i.toTopologicalSpace] ↑v.integer

Tactic:
simp only [integer, Subring.coe_set_mk, Subsemiring.coe_set_mk, Submonoid.coe_set_mk,
    Subsemigroup.coe_set_mk, ← v.restrict_le_one_iff]

Goal state after:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ IsClosed[_i.toTopologicalSpace] {x | v.restrict x ≤ 1}
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case mp
R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
⊢ IsNontrivial R → v.IsNontrivial

Tactic:
rintro ⟨r, hr, hr'⟩
    induction r using ValueGroupWithZero.ind with | mk r s
    have hγ : v r ≠ 0 := by simpa [Valuation.Compatible.vle_iff_le (v := v)] using hr
    have hγ' : v r ≤ v s → v r < v s := by
      simpa [Valuation.Compatible.vle_iff_le (v := v)] using hr'
    by_cases hr : v r = 1
    · exact ⟨s, by simp, fun h ↦ by simp [h, hr] at hγ'⟩
    · exact ⟨r, by simpa using hγ, hr⟩

Goal state after:
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 Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
⊢ IsOpen[_t] ↑v.integer

Tactic:
simp only [integer, Subring.coe_set_mk, Subsemiring.coe_set_mk, Submonoid.coe_set_mk,
    Subsemigroup.coe_set_mk, ← v.restrict_le_one_iff]

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
⊢ IsOpen[_t] {x | v.restrict x ≤ 1}
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 Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
⊢ IsClosed[_t] ↑v.integer

Tactic:
simp only [integer, Subring.coe_set_mk, Subsemiring.coe_set_mk, Submonoid.coe_set_mk,
    Subsemigroup.coe_set_mk, ← v.restrict_le_one_iff]

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
⊢ IsClosed[_t] {x | v.restrict x ≤ 1}
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
γ : (ofClass v).ValueGroup₀
x : R
⊢ (orderMonoidIso v) ((valuation R) x) < (orderMonoidIso v) ((orderMonoidIso v).symm γ) ↔ v.restrict x < γ

Tactic:
by simp [v.restrict_def x]

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

Goal state before:
pp: case pos
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : P = ⊥
⊢ Submodule.IsPrincipal P

Tactic:
rw [h_ne_bot]; exact bot_isPrincipal

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

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
⊢ v (x⁻¹ - y⁻¹) < ↑γ

Tactic:
have hyp1' : v (x - y) * (v y * v y)⁻¹ < γ := mul_inv_lt_of_lt_mul₀ hyp1

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
⊢ v (x⁻¹ - y⁻¹) < ↑γ
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : v.restrict z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑a = (fun x ↦ x * x₀) y
⊢ ↑(a * z₀⁻¹) ∈ V

Tactic:
have : (z₀⁻¹ : K) = (z₀ : hat K)⁻¹ := map_inv₀ (Completion.coeRingHom : K →+* hat K) z₀

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : v.restrict z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑a = (fun x ↦ x * x₀) y
this : ↑z₀⁻¹ = (↑z₀)⁻¹
⊢ ↑(a * z₀⁻¹) ∈ V
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : hat K
⊢ extensionValuation x = 0 ↔ x = 0

Tactic:
rw [Valuation.zero_iff]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
h : IsIntegral R W
⊢ (valuation K (maximalIdeal R)) W.Δ ≤ 1

Tactic:
choose r hr using Δ_integral_of_isIntegral R W
      rw [← hr]
      exact valuation_le_one (maximalIdeal R) r

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

Tactic:
rw [intValuationDef, if_pos hxy]; exact zero_le

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
f g : R⟦X⟧
⊢ (mk fun n ↦ a ^ n * (coeff n) (f * g)) = (mk fun n ↦ a ^ n * (coeff n) f) * mk fun n ↦ a ^ n * (coeff n) g

Tactic:
ext
    rw [PowerSeries.coeff_mul, PowerSeries.coeff_mk, PowerSeries.coeff_mul, Finset.mul_sum]
    apply sum_congr rfl
    simp only [coeff_mk, Prod.forall, mem_antidiagonal]
    intro b c H
    rw [← H, pow_add, mul_mul_mul_comm]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
φ : R →+* S
r : R
f : R⟦X⟧
⊢ (rescale (φ r)) ((map φ) f) = (map φ) ((rescale r) f)

Tactic:
ext n
  simp [coeff_rescale, coeff_map, map_mul, map_pow]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
⊢ ∏ x ∈ s, constantCoeff f = 0

Tactic:
prod_const

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
⊢ constantCoeff f ^ #s = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case h
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
d : R
hd : d ∈ nonZeroDivisors R
hd0 : d ≠ 0
z : R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K (d * z) ⟨d, hd⟩) ≤ 1
hx :
  (algebraMap R K) ↑(d * z, ⟨d, hd⟩).2 * IsLocalization.mk' K (d * z) ⟨d, hd⟩ = (algebraMap R K) d * (algebraMap R K) z
hn0 : d * z ≠ 0
this : Ideal.span {d} ∣ Ideal.span {d * z}
⊢ (algebraMap R K) z = IsLocalization.mk' K (d * z) ⟨d, hd⟩

Tactic:
mul_eq_mul_left_iff

Goal state after:
case h
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
d : R
hd : d ∈ nonZeroDivisors R
hd0 : d ≠ 0
z : R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K (d * z) ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K (d * z) ⟨d, hd⟩ = (algebraMap R K) z ∨ (algebraMap R K) ↑(d * z, ⟨d, hd⟩).2 = 0
hn0 : d * z ≠ 0
this : Ideal.span {d} ∣ Ideal.span {d * z}
⊢ (algebraMap R K) z = IsLocalization.mk' K (d * z) ⟨d, hd⟩
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ¬IsField A⟦X⟧

Tactic:
Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top

Goal state after:
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ∃ I, ⊥ < I ∧ I < ⊤
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case neg.right
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff d_1) ((monomial d) a) = 0

Tactic:
intro b hb
      rw [coeff_monomial, if_neg]
      rintro rfl
      exact hb.false

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
hs : IsLowerSet ↑s
k : ℕ
p : MvPowerSeries σ R
n : ℕ
hmn : 1 ≤ n
ih : (truncFinset R s) (↑((truncFinset R s) p) ^ n) = (truncFinset R s) (p ^ n)
x : σ →₀ ℕ
hx : x ∈ s
⊢ MvPolynomial.coeff x ((truncFinset R s) (p ^ n) * (truncFinset R s) ↑((truncFinset R s) p)) = (coeff x) (p ^ (n + 1))

Tactic:
truncFinset_truncFinset
        (by rfl),

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
hs : IsLowerSet ↑s
k : ℕ
p : MvPowerSeries σ R
n : ℕ
hmn : 1 ≤ n
ih : (truncFinset R s) (↑((truncFinset R s) p) ^ n) = (truncFinset R s) (p ^ n)
x : σ →₀ ℕ
hx : x ∈ s
⊢ MvPolynomial.coeff x ((truncFinset R s) (p ^ n) * (truncFinset R s) p) = (coeff x) (p ^ (n + 1))
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h : (trunc' R n) f = (trunc' R n) g
f' : MvPowerSeries σ R
⊢ (coeff n) f' = if n ≤ n then (coeff n) f' else 0

Tactic:
if_pos le_rfl

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h : (trunc' R n) f = (trunc' R n) g
f' : MvPowerSeries σ R
⊢ (coeff n) f' = (coeff n) f'
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
h : ↑f.order.toNat = f.order
⊢ ∃ d, (coeff d) f ≠ 0 ∧ ↑(degree d) = f.order

Tactic:
simp_rw [degree_eq_weight_one]
  exact exists_coeff_ne_zero_and_weightedOrder _ h

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

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

Tactic:
rw [coeff_weightedHomogeneousComponent, if_neg hd]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ (trunc n.succ) f = (trunc n) f + (Polynomial.monomial n) ((coeff n) f)

Tactic:
by
  rw [trunc_apply, Ico_zero_eq_range, sum_range_succ, trunc_apply, Ico_zero_eq_range]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ (v.intAdicAbv hb) r < 1 ↔ r ∈ v.asIdeal

Tactic:
simpa [intAdicAbv, intAdicAbvDef, toNNReal_lt_one_iff hb] using intValuation_lt_one_iff_mem v r

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

Goal state before:
pp: case neg.inr.inl
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.1 < φ.order.toNat
⊢ (coeff ij.1) φ * (coeff ij.2) ψ = 0

Tactic:
rw [coeff_of_lt_order_toNat ij.1 h', zero_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), (coeff n) p ∈ T
d : ℕ
hd : ↑d < (p.toSubring T hp).order
⊢ (coeff d) p = 0

Tactic:
by simp [coeff_of_lt_order d hd, ← coeff_toSubring p T hp]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : UniformSpace R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : UniformSpace S
a : σ → S
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : IsUniformAddGroup R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : CompleteSpace S
inst✝⁴ : T2Space S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ha : HasEval a
⊢ Continuous[instTopologicalSpace R, inst✝⁹.toTopologicalSpace] ⇑(aeval ha)

Tactic:
by
  rw [coe_aeval]
  exact continuous_eval₂ (continuous_algebraMap R S) ha

Goal state after:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case a
⊢ #(CauSeq ℚ abs) ≤ 𝔠

Tactic:
apply (mk_subtype_le _).trans_eq

Goal state after:
case a
⊢ #(ℕ → ℚ) = 𝔠