mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.b₄ = -W.a₄ + W.a₁ * W.a₃

Tactic:
rw [b₄]

Goal state after:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ 2 * W.a₄ + W.a₁ * W.a₃ = -W.a₄ + W.a₁ * W.a₃
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
hU : IsCompact ↑U
s : ↑Γ(D.obj i, U)
hs : (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) s = 0
this : CompactSpace ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
H : (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U
j : Over i
f : j ⟶ Over.mk (𝟙 i)
hf :
  (ConcreteCategory.hom (Scheme.Hom.appTop ((opensDiagram D i U).map f)))
      ((ConcreteCategory.hom ((D.obj i).presheaf.map (homOfLE ⋯).op)) s) =
    0
⊢ ∃ j f, (ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) s = 0

Tactic:
dsimp at hf

Goal state after:
I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
hU : IsCompact ↑U
s : ↑Γ(D.obj i, U)
hs : (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) s = 0
this : CompactSpace ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
H : (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U
j : Over i
f : j ⟶ Over.mk (𝟙 i)
hf :
  (ConcreteCategory.hom
        (Scheme.Hom.appTop (Scheme.Hom.resLE (D.map (Over.Hom.left f)) (D.map (𝟙 i) ⁻¹ᵁ U) (D.map j.hom ⁻¹ᵁ U) ⋯)))
      ((ConcreteCategory.hom ((D.obj i).presheaf.map (homOfLE ⋯).op)) s) =
    0
⊢ ∃ j f, (ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) s = 0
Module: Mathlib.LinearAlgebra.FreeModule.Norm

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
⊢ Associated ((Algebra.norm R) f) (∏ i, smithCoeffs b (span {f}) ⋯ i)

Tactic:
rw [← Matrix.det_diagonal, ← LinearMap.det_toLin b']

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
⊢ Associated ((Algebra.norm R) f) (LinearMap.det ((Matrix.toLin b' b') (Matrix.diagonal (smithCoeffs b (span {f}) ⋯))))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ (Algebra.norm R[X]) (p • 1 + q • (mk W') Y) =
    p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)

Tactic:
simp_rw [Algebra.norm_eq_matrix_det <| CoordinateRing.basis W', Matrix.det_fin_two,
    Algebra.leftMulMatrix_eq_repr_mul, basis_zero, mul_one, basis_one, smul_basis_mul_Y, map_add,
    Finsupp.add_apply, map_smul, Finsupp.smul_apply, ← basis_zero, ← basis_one,
    Basis.repr_self_apply, if_pos, one_ne_zero, if_false, smul_eq_mul]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ (p * 1 + q * 0) *
        ((q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) * if 0 = 1 then 1 else 0) +
          (p - q * (C W'.a₁ * X + C W'.a₃)) * 1) -
      (q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) * 1 + (p - q * (C W'.a₁ * X + C W'.a₃)) * 0) *
        ((p * if 0 = 1 then 1 else 0) + q * 1) =
    p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsShortNF
⊢ W.Δ = -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)

Tactic:
rw [Δ_of_isCharNeTwoNF, a₂_of_isShortNF]
  ring1

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

Goal state before:
pp: case h.a₂
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ ({ u := 1, r := 0, s := s, t := 0 } • E).a₂ = E'.a₂

Tactic:
simp_rw [variableChange_a₂, inv_one, Units.val_one, a₁_of_isCharTwoJNeZeroNF]
    linear_combination -hs + E.a₂ * CharP.cast_eq_zero F 2

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

Goal state before:
pp: F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
⊢ W.j = -W.a₂ ^ 3 / W.a₆

Tactic:
have h := W.Δ'.ne_zero
  rw [coe_Δ', Δ_of_isCharThreeJNeZeroNF_of_char_three] at h
  rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ',
    c₄_of_isCharThreeJNeZeroNF_of_char_three, Δ_of_isCharThreeJNeZeroNF_of_char_three,
    div_eq_div_iff h (right_ne_zero_of_mul h)]
  ring1

Goal state after:
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
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
i' : I
fi'i : i' ⟶ i
hi' : ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2
𝒱' : ↥s → (D.obj i').Opens := fun x ↦ D.map fi'i ⁻¹ᵁ 𝒱 x
h𝒱'𝒰 : ∀ (j : ↥s), c.π.app i' ⁻¹ᵁ 𝒱' j = (↑↑j).1
x✝ : ∀ (j : ↥s) (k : Over i'), IsAffine ((opensDiagram D i' (𝒱' j)).obj k)
j : ↥s
k : Over i'
⊢ D.map k.hom ⁻¹ᵁ 𝒱' j ≤ t.app k.left ⁻¹ᵁ ↑(↑(↑↑j).2).2

Tactic:
by
        refine (Hom.preimage_mono _ (hi' _)).trans ?_
        simp only [Functor.const_obj_obj, ← Hom.comp_preimage, t.naturality,
          Functor.const_obj_map, Category.comp_id, le_refl]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
⊢ W.ΨSq n ≠ 0

Tactic:
by_cases hn : 1 < n.natAbs
  · exact ne_zero_of_natDegree_gt <| W.natDegree_ΨSq_pos hn h
  · rcases hm : n.natAbs with _ | m
    · push_cast [Int.natAbs_eq_zero.mp hm, ne_self_iff_false] at h
    · rcases Int.natAbs_eq_iff.mp hm with rfl | rfl <;>
        rw [hm, Nat.lt_add_left_iff_pos, Nat.not_lt_eq, Nat.le_zero] at hn <;>
        push_cast [hn, ΨSq_neg, ΨSq_one] <;>
        exact fun h' => h <| C_injective <| by push_cast [hn, C_neg, C_1, h', neg_zero, C_0]; rfl

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : P y ^ 2 = P x ^ 3 ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W'.a₁ * P x * P y ≠ 0)
hPz : P z = 0
hPx : P x ≠ 0
hPy : P y = 0
⊢ False

Tactic:
hPy,

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : 0 ^ 2 = P x ^ 3 ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * 0 ≠ 0 ∨ W'.a₁ * P x * 0 ≠ 0)
hPz : P z = 0
hPx : P x ≠ 0
hPy : P y = 0
⊢ False
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : Semiring R
inst✝² : ValuativeRel R
inst✝¹ : IsDiscrete R
inst✝ : IsNontrivial R
a : ValueGroupWithZero R
ha : a = 0
⊢ (uniformizer R)⁻¹ ≤ a ↔ 1 < a

Tactic:
simp [ha]

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
⊢ 0⁻¹ = 0

Tactic:
by simp only [Inv.inv, ite_true]

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

Goal state before:
pp: Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝¹ : Ring A
v : Valuation A Γ
inst✝ : v.IsRankOneDiscrete
⊢ IsCyclic ↥(zpowers (generator v))

Tactic:
exact isCyclic_zpowers (generator v)

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: e : ℤ ≃+ ℤ
he : ¬IsOfFinAddOrder (e 1)
⊢ e 1 = 1 ∨ -e 1 = 1

Tactic:
rw [← AddSubgroup.zmultiples_eq_zmultiples_iff he]

Goal state after:
e : ℤ ≃+ ℤ
he : ¬IsOfFinAddOrder (e 1)
⊢ AddSubgroup.zmultiples (e 1) = AddSubgroup.zmultiples 1
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case h.right
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₁ : x ∈ M₁
y : K
H₁ : v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
left✝ : y ∈ M₀
y_in₁ : y ∈ M₁
x_in₀ : ↑γ₀ ≤ v.restrict x
⊢ v.restrict (y⁻¹ - x⁻¹) < ↑γ

Tactic:
apply Valuation.inversion_estimate

Goal state after:
case h.right.y_ne
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₁ : x ∈ M₁
y : K
H₁ : v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
left✝ : y ∈ M₀
y_in₁ : y ∈ M₁
x_in₀ : ↑γ₀ ≤ v.restrict x
⊢ x ≠ 0

case h
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₁ : x ∈ M₁
y : K
H₁ : v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
left✝ : y ∈ M₀
y_in₁ : y ∈ M₁
x_in₀ : ↑γ₀ ≤ v.restrict x
⊢ v.restrict (y - x) < min (↑γ * (v.restrict x * v.restrict x)) (v.restrict x)
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mp
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y | y ∈ closure {b ^ n} ∧ 1 < y} b
this✝ : closure {b ^ n} = closure {b}
this : (∃ n_1, (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
key : m = 1 ∧ n = 1 ∨ m = -1 ∧ n = -1
⊢ |b ^ n|ₘ = b ∧ 1 < b

Tactic:
rcases key with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ <;>
    simp [this.right.le, this.right, mabs]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
hy' : 0 < y
z : G
hz : z ∈ {x | 0 ≤ x}
hz' : ⟨z, hz⟩ ∈ {x | ⟨0, ⋯⟩ < x}
hz'' : ∀ x ∈ {x | ⟨0, ⋯⟩ < x}, ¬x < ⟨z, hz⟩
w : G
hw : ↑⟨0, ⋯⟩ < w
hw' : w < ↑⟨z, hz⟩
⊢ False

Tactic:
exact hz'' ⟨w, hw.le⟩ hw hw'

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case neg
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
x y : G
hy0 : 0 < y
H : ∀ (n : ℕ), n • y < x
n : ℕ
hz : ∀ x_1 ∈ range fun n ↦ ⟨x - n • y, ⋯⟩, ¬x_1 < (fun n ↦ ⟨x - n • y, ⋯⟩) n
⊢ False

Tactic:
refine hz ⟨x - (n + 1) • y, sub_nonneg.mpr (H _).le⟩ ⟨_, rfl⟩ ?_

Goal state after:
case neg
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
x y : G
hy0 : 0 < y
H : ∀ (n : ℕ), n • y < x
n : ℕ
hz : ∀ x_1 ∈ range fun n ↦ ⟨x - n • y, ⋯⟩, ¬x_1 < (fun n ↦ ⟨x - n • y, ⋯⟩) n
⊢ ⟨x - (n + 1) • y, ⋯⟩ < (fun n ↦ ⟨x - n • y, ⋯⟩) n
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
⊢ ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃+o ℤ)

Tactic:
by
  suffices Set.WellFoundedOn {x : G | 0 ≤ x} (· < ·) ↔ Nonempty (G ≃+o ℤ) by
    rw [← this]
    refine ⟨fun h ↦ (h.mapsTo (· + g) ?_).mono' ?_, fun h ↦ (h.mapsTo (· - g) ?_).mono' ?_⟩ <;>
    · try intro
      simp [Function.onFun]
  constructor
  · intro h
    replace h : WellFounded (α := {x : G | 0 ≤ x}) (· < ·) := h
    rw [WellFounded.wellFounded_iff_has_min] at h
    by_cases! H : ∀ (x : G) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y -- Archimedean
    · replace H : Archimedean G := ⟨H⟩
      rw [LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered]
      intro hd
      obtain ⟨y, hy⟩ := exists_ne (0 : G)
      wlog! hy' : 0 < y generalizing y
      · refine this (-y) ?_ ?_
        · simp [hy]
        · simp [lt_of_le_of_ne hy' hy]
      obtain ⟨⟨z, hz⟩, hz', hz''⟩ := h ({x | ⟨0, le_rfl⟩ < x}) ⟨⟨y, hy'.le⟩, hy'⟩
      obtain ⟨w, hw, hw'⟩ := exists_between hz'
      exact hz'' ⟨w, hw.le⟩ hw hw'
    · exfalso
      obtain ⟨x, y, hy0, H⟩ := H
      obtain ⟨_, ⟨n, rfl⟩, hz⟩ :=
        h (Set.range (fun n : ℕ ↦ ⟨x - n • y, sub_nonneg.mpr (H _).le⟩)) (range_nonempty _)
      refine hz ⟨x - (n + 1) • y, sub_nonneg.mpr (H _).le⟩ ⟨_, rfl⟩ ?_
      simp [add_smul, hy0]
  · rintro ⟨f⟩
    have : LocallyFiniteOrder G := LocallyFiniteOrder.ofOrderIsoClass f
    exact BddBelow.wellFoundedOn_lt ⟨0, by simp [mem_lowerBounds]⟩

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
⊢ ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ))

Tactic:
suffices Set.WellFoundedOn {x : G₀ | g ≤ x} (· < ·) ↔
    Set.WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} (· < ·) by
    rw [this, LinearOrderedCommGroup.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete]
    refine Nonempty.congr (fun f ↦ ⟨?_, ?_⟩) (fun f ↦ ⟨?_, ?_⟩)
    · exact WithZero.withZeroUnitsEquiv.symm.trans f.withZero
    · intro a b
      rcases eq_or_ne a 0 with rfl | ha
      · simp [WithZero.withZeroUnitsEquiv]
      rcases eq_or_ne b 0 with rfl | hb
      · simp [WithZero.withZeroUnitsEquiv]
      simp [WithZero.withZeroUnitsEquiv, ha, hb, ← Units.val_le_val]
    · exact MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans f)
    · intros
      rw [← WithZero.coe_le_coe]
      simp

Goal state after:
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
⊢ ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
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 Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
hx : (restrict₀ (ofClass v)) x = a
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : (restrict₀ (ofClass v)) y = b
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
hxy : embedding ((restrict₀ (ofClass v)) xy) = embedding (a * b)
⊢ extensionValuation.restrict ↑xy = extensionValuation.restrict ↑x * extensionValuation.restrict ↑y

Tactic:
apply_fun embedding at hx

Goal state after:
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
hy : (restrict₀ (ofClass v)) y = b
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
hxy : embedding ((restrict₀ (ofClass v)) xy) = embedding (a * b)
hx : embedding ((restrict₀ (ofClass v)) x) = embedding a
⊢ extensionValuation.restrict ↑xy = extensionValuation.restrict ↑x * extensionValuation.restrict ↑y
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : φ * X = ψ * X
⊢ φ = ψ

Tactic:
by
  rw [PowerSeries.ext_iff] at h ⊢
  intro n
  simpa using h (n + 1)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : X * φ = X * ψ
⊢ φ = ψ

Tactic:
by
  rw [PowerSeries.ext_iff] at h ⊢
  intro n
  simpa using h (n + 1)

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

Goal state before:
pp: S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(map f)

Tactic:
intro g
  use PowerSeries.mk fun k ↦ Function.surjInv hf (PowerSeries.coeff k g)
  ext k
  simp only [Function.surjInv, coeff_map, coeff_mk]
  exact Classical.choose_spec (hf (coeff k g))

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
hab : valueGroup₀_hom_extensionValuation a = valueGroup₀_hom_extensionValuation b
x : K := ⋯.choose
hx_def : x = ⋯.choose
hx : (restrict₀ (ofClass v)) ⋯.choose = a
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : (restrict₀ (ofClass v)) ⋯.choose = b
⊢ embedding a = embedding b

Tactic:
apply_fun embedding at hx

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
hab : valueGroup₀_hom_extensionValuation a = valueGroup₀_hom_extensionValuation b
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : (restrict₀ (ofClass v)) ⋯.choose = b
hx : embedding ((restrict₀ (ofClass v)) ⋯.choose) = embedding a
⊢ embedding a = embedding b
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
⊢ v.asIdeal ∣ Ideal.span {r} ↔ r ∈ v.asIdeal

Tactic:
Ideal.dvd_span_singleton

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
⊢ r ∈ v.asIdeal ↔ r ∈ v.asIdeal
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
⊢ v.asIdeal ^ n ∣ Ideal.span {r} ↔ r ∈ v.asIdeal ^ n

Tactic:
Ideal.dvd_span_singleton

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
⊢ r ∈ v.asIdeal ^ n ↔ r ∈ v.asIdeal ^ n
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ v.asIdeal ^ 2
⊢ Associates.mk (Ideal.span {π}) ≠ 0

Tactic:
Associates.mk_ne_zero'

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ v.asIdeal ^ 2
⊢ π ≠ 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : 0 ∉ v.asIdeal ^ 2
h : π = 0
⊢ False

Tactic:
exact notMem (Submodule.zero_mem (v.asIdeal ^ 2))

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ ↑f = ↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1}).symm f)

Tactic:
set g := (MvPolynomial.uniqueAlgEquiv R PUnit).symm f

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
g : MvPolynomial PUnit.{1} R := (MvPolynomial.uniqueAlgEquiv R PUnit.{1}).symm f
⊢ ↑f = ↑g
Module: Mathlib.RingTheory.MvPowerSeries.Order

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

Tactic:
by_contra! H

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0
H : weightedOrder w f < ↑n
⊢ False
Module: Mathlib.RingTheory.MvPowerSeries.Order

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

pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
⊢ ((∃ d, (coeff d) f ≠ 0 ∧ (weight w) d = n) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0) →
    weightedOrder w f = ↑n

Tactic:
· intro h
    obtain ⟨d, hd⟩ := f.exists_coeff_ne_zero_and_weightedOrder w (by simp only [h, toNat_natCast])
    exact ⟨⟨d, by simpa [h, Nat.cast_inj, ne_eq] using hd⟩,
      fun e he ↦ f.coeff_eq_zero_of_lt_weightedOrder w (by simp only [h, Nat.cast_lt, he])⟩

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
⊢ ((∃ d, (coeff d) f ≠ 0 ∧ (weight w) d = n) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0) →
    weightedOrder w f = ↑n
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : σ → R
⊢ (MvPowerSeries.monomial e) (e.prod fun s n ↦ r s ^ n) = (MvPowerSeries.monomial e) ((e.prod fun s n ↦ r s ^ n) • 1)

Tactic:
smul_eq_mul,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : σ → R
⊢ (MvPowerSeries.monomial e) (e.prod fun s n ↦ r s ^ n) = (MvPowerSeries.monomial e) ((e.prod fun s n ↦ r s ^ n) * 1)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_4
R : Type u_5
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ (MvPowerSeries.monomial e) (r ^ e.sum fun x n ↦ n) = (MvPowerSeries.monomial e) ((e.prod fun s n ↦ r ^ n) • 1)

Tactic:
smul_eq_mul,

Goal state after:
σ : Type u_4
R : Type u_5
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ (MvPowerSeries.monomial e) (r ^ e.sum fun x n ↦ n) = (MvPowerSeries.monomial e) ((e.prod fun s n ↦ r ^ n) * 1)
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 Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
a : K
ha : v a = γ
⊢ v ↑a = γ

Tactic:
simp [ha]

Goal state after: