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

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift ⟦Q⟧
hQz : Q z = 0
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦Q⟧

Tactic:
rw [addMap_eq, add_of_Z_eq_zero hP hQ hPz hQz,
      smul_eq _ <| (isUnit_X_of_Z_eq_zero hP hPz).pow 2, Quotient.eq]

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift ⟦Q⟧
hQz : Q z = 0
⊢ (MulAction.orbitRel Fˣ (Fin 3 → F)) ![1, 1, 0] Q
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : P z = 0
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦P⟧

Tactic:
rw [addMap_eq, add_of_Z_eq_zero hP hQ hPz hQz,
      smul_eq _ <| (isUnit_X_of_Z_eq_zero hP hPz).pow 2, Quotient.eq]

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : P z = 0
⊢ (MulAction.orbitRel Fˣ (Fin 3 → F)) ![1, 1, 0] P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ W.addX P Q = W.addX P Q * (P z * Q z) ^ 2 / (P z * Q z) ^ 2

Tactic:
mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ W.addX P Q = W.addX P Q
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case some
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Jacobian R
W : Jacobian F
inst✝ : DecidableEq F
x✝ y✝ : F
h✝ : W.toAffine.Nonsingular x✝ y✝
⊢ { point := ⟦![x✝, y✝, 1]⟧, nonsingular := ⋯ }.toAffineLift = Affine.Point.some x✝ y✝ h✝

Tactic:
toAffineLift_some

Goal state after:
case some
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Jacobian R
W : Jacobian F
inst✝ : DecidableEq F
x✝ y✝ : F
h✝ : W.toAffine.Nonsingular x✝ y✝
⊢ Affine.Point.some x✝ y✝ ⋯ = Affine.Point.some x✝ y✝ h✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

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

Tactic:
(rw [addX]; ring1)

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

Goal state before:
pp: R K : Type u
inst✝² : Ring R
inst✝¹ : DivisionRing K
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
s : Set R
γ : (ofClass v).ValueGroup₀ˣ
⊢ True ∧ ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ)) ⊆ s ↔ {x | v x < embedding ↑γ} ⊆ s

Tactic:
rw [true_and]; rfl

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addX P Q = W.addX P Q * (P z * Q z) ^ 2 / (P z * Q z) ^ 2

Tactic:
mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addX P Q = W.addX P Q
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
a b : R
hab : a ≤ᵥ b
n : ℕ
⊢ a ^ n ≤ᵥ b ^ n

Tactic:
by
  induction n with
  | zero => simp
  | succ _ hn => simp [pow_succ, mul_vle_mul hn hab]

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : Ring R
inst✝⁶ : ValuativeRel R
K : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : ValuativeRel K
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : TopologicalSpace R
v : Valuation R Γ₀
inst✝¹ : v.Compatible
inst✝ : IsValuativeTopology R
⊢ IsTopologicalAddGroup R

Tactic:
have cts_add : ContinuousConstVAdd R R :=
    ⟨fun x ↦ continuous_iff_continuousAt.2 fun z ↦
      (((valuation R).hasBasis_nhds z).tendsto_iff ((valuation R).hasBasis_nhds (x + z))).2
        fun γ _ ↦ ⟨γ, trivial, fun y hy ↦ by simpa using hy⟩⟩
  have basis := (valuation R).hasBasis_nhds_zero
  refine .of_comm_of_nhds_zero ?_ ?_ fun x₀ ↦ (map_eq_of_inverse (-x₀ + ·) ?_ ?_ ?_).symm
  · exact (basis.prod_self.tendsto_iff basis).2 fun γ _ ↦
      ⟨γ, trivial, fun ⟨_, _⟩ hx ↦ (valuation R).restrict.map_add_lt hx.left hx.right⟩
  · exact (basis.tendsto_iff basis).2 fun γ _ ↦ ⟨γ, trivial, fun y hy ↦ by simpa using hy⟩
  · ext; simp
  · simpa [ContinuousAt] using (cts_add.1 x₀).continuousAt (x := 0)
  · simpa [ContinuousAt] using (cts_add.1 (-x₀)).continuousAt (x := x₀)

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 Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = Units.mk0 (v ↑r) hr₀
⊢ v ↑π.val ^ m = ↑(Units.mk0 (v ↑π.val) ⋯ ^ m)

Tactic:
simp [Units.val_zpow_eq_zpow_val, Units.val_mk0]

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

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Ring R
v : Valuation R Γ₀
S : Type u_3
inst✝¹ : Ring S
Λ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Λ₀
w : Valuation S Λ₀
s : Set (WithVal v)
x : WithVal v
⊢ (∃ γ, {y | Valued.v.restrict (y - x) < ↑γ} ⊆ s) ↔ ∃ γ, {a | (ValuativeRel.valuation (WithVal v)) (-x + a) < ↑γ} ⊆ s

Tactic:
let e := ValuativeRel.ValueGroupWithZero.orderMonoidIso (valuation v)

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Ring R
v : Valuation R Γ₀
S : Type u_3
inst✝¹ : Ring S
Λ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Λ₀
w : Valuation S Λ₀
s : Set (WithVal v)
x : WithVal v
e : ValuativeRel.ValueGroupWithZero (WithVal v) ≃*o (MonoidWithZeroHom.ofClass (valuation v)).ValueGroup₀ :=
  ValuativeRel.ValueGroupWithZero.orderMonoidIso (valuation v)
⊢ (∃ γ, {y | Valued.v.restrict (y - x) < ↑γ} ⊆ s) ↔ ∃ γ, {a | (ValuativeRel.valuation (WithVal v)) (-x + a) < ↑γ} ⊆ s
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
⊢ ContinuousAt (⇑(equiv v)) 0

Tactic:
simp_rw [ContinuousAt, map_zero, (Valued.hasBasis_nhds_zero _ _).tendsto_iff
    (Valued.hasBasis_nhds_zero _ _), true_and, forall_const]

Goal state after:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
⊢ ∀ (ib : (ofClass Valued.v).ValueGroup₀ˣ),
    ∃ ia, ∀ x ∈ {x | Valued.v.restrict x < ↑ia}, (equiv v) x ∈ {x | Valued.v.restrict x < ↑ib}
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case neg
Γ : 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 = ⊥
π : v.Uniformizer := ⋯.some
x : ↥v.valuationSubring
hx_mem : x ∈ P
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : ↑x = ↑(π.val ^ n) * ↑↑u
hn : ¬n = 0
⊢ Submodule.IsPrincipal P

Tactic:
rw [← Subring.coe_mul, SetLike.coe_eq_coe] at hu
      rw [hu, Ideal.mul_unit_mem_iff_mem P u.isUnit,
        IsPrime.pow_mem_iff_mem hP _ (pos_iff_ne_zero.mpr hn),
        ← Ideal.span_singleton_le_iff_mem] at hx_mem
      replace hx_mem := π.is_generator ▸ hx_mem
      rw [← Ideal.IsMaximal.eq_of_le (IsLocalRing.maximalIdeal.isMaximal K₀) hP.ne_top hx_mem]
      exact ⟨π.1, π.is_generator⟩

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

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
⊢ ContinuousAt (⇑(equiv v).symm) 0

Tactic:
simp_rw [ContinuousAt, map_zero, (Valued.hasBasis_nhds_zero _ _).tendsto_iff
    (Valued.hasBasis_nhds_zero _ _), true_and, forall_const]

Goal state after:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
⊢ ∀ (ib : (ofClass Valued.v).ValueGroup₀ˣ),
    ∃ ia, ∀ x ∈ {x | Valued.v.restrict x < ↑ia}, (equiv v).symm x ∈ {x | Valued.v.restrict x < ↑ib}
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Jacobian R
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
P Q : Fin 3 → A
⊢ (W'⁄B).addX (⇑f ∘ P) (⇑f ∘ Q) = f ((W'⁄A).addX P Q)

Tactic:
rw [← RingHom.coe_coe, ← map_addX, map_baseChange]

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

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
h_res : v.restrict.IsEquiv w.restrict
⊢ ContinuousAt (⇑(RingHom.id R)) 0

Tactic:
simp_rw [ContinuousAt, map_zero, (Valued.hasBasis_nhds_zero _ _).tendsto_iff
    (Valued.hasBasis_nhds_zero _ _), true_and, forall_const]

Goal state after:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
h_res : v.restrict.IsEquiv w.restrict
⊢ ∀ (ib : (ofClass Valued.v).ValueGroup₀ˣ),
    ∃ ia, ∀ x ∈ {x | Valued.v.restrict x < ↑ia}, (RingHom.id R) x ∈ {x | Valued.v.restrict x < ↑ib}
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation π ^ m ≤ 1
v_π_lt_one : (maximalIdeal A).intValuation π < 1
⊢ m ≤ n

Tactic:
have v_π_ne_zero : (maximalIdeal A).intValuation π ≠ 0 := intValuation_ne_zero _ _ hπ.ne_zero

Goal state after:
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation π ^ m ≤ 1
v_π_lt_one : (maximalIdeal A).intValuation π < 1
v_π_ne_zero : (maximalIdeal A).intValuation π ≠ 0
⊢ m ≤ n
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
⊢ ContinuousAt (⇑v.restrict) x

Tactic:
rcases eq_or_ne x 0 with (rfl | h)

Goal state after:
case inl
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ ContinuousAt (⇑v.restrict) 0

case inr
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
⊢ ContinuousAt (⇑v.restrict) x
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Continuous[hv.toTopologicalSpace, _] ⇑v.restrict

Tactic:
by
  rw [continuous_iff_continuousAt]
  intro x
  rcases eq_or_ne x 0 with (rfl | h)
  · rw [ContinuousAt, map_zero, WithZeroTopology.tendsto_zero]
    intro γ hγ
    rw [Filter.Eventually, Valued.mem_nhds_zero]
    use Units.mk0 γ hγ; rfl
  · have v_ne : (v.restrict x : ValueGroup₀ (.ofClass hv.v)) ≠ 0 :=
      (Valuation.ne_zero_iff _).mpr h
    rw [ContinuousAt, WithZeroTopology.tendsto_of_ne_zero v_ne]
    simp_rw [v.restrict_inj]
    apply Valued.locally_const (by simpa [restrict₀_apply] using v_ne)

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 Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective ⇑v
x : K
⊢ ContinuousAt (⇑v) x

Tactic:
rcases eq_or_ne x 0 with (rfl | h)

Goal state after:
case inl
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective ⇑v
⊢ ContinuousAt (⇑v) 0

case inr
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective ⇑v
x : K
h : x ≠ 0
⊢ ContinuousAt (⇑v) x
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
⊢ False

Tactic:
obtain ⟨_, ⟨n, rfl⟩, hz⟩ :=
        h (Set.range (fun n : ℕ ↦ ⟨x - n • y, sub_nonneg.mpr (H _).le⟩)) (range_nonempty _)

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
⊢ False
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case hp
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ IsClosed {x | extension (x.1 + x.2) ≤ extension x.1 ∨ extension (x.1 + x.2) ≤ extension x.2}

pp: case ih
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (a b : K), extension (↑a + ↑b) ≤ extension ↑a ∨ extension (↑a + ↑b) ≤ extension ↑b

Tactic:
· have cont : Continuous (Valued.extension : hat K → _) := Valued.continuous_extension
      exact (isClosed_le (by fun_prop) <| cont.comp continuous_fst).union
          (isClosed_le (by fun_prop) <| cont.comp continuous_snd)

Goal state after:
case ih
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (a b : K), extension (↑a + ↑b) ≤ extension ↑a ∨ extension (↑a + ↑b) ≤ extension ↑b
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
⊢ ∃ r, extensionValuation x = v r

Tactic:
rcases eq_or_ne x 0 with (rfl | h)

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ ∃ r, extensionValuation 0 = v r

case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : hat K
h : x ≠ 0
⊢ ∃ r, extensionValuation x = v r
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_1
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ MapsTo (fun x ↦ x⁻¹) {x | g⁻¹ ≤ x} ({x | x ≤ g} \ {0})

pp: case refine_2
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ ∀ a ∈ {x | g⁻¹ ≤ x}, ∀ b ∈ {x | g⁻¹ ≤ x}, a < b → Function.onFun (fun x1 x2 ↦ x1 > x2) (fun x ↦ x⁻¹) a b

pp: case refine_3
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ MapsTo (fun x ↦ x⁻¹) ({x | x ≤ g} \ {0}) {x | g⁻¹ ≤ x}

pp: case refine_4
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ∀ a ∈ {x | x ≤ g} \ {0}, ∀ b ∈ {x | x ≤ g} \ {0}, a > b → Function.onFun (fun x1 x2 ↦ x1 < x2) (fun x ↦ x⁻¹) a b

Tactic:
· intro x
    rcases eq_or_ne x 0 with rfl | hx
    · simp [hg]
    simp only [mem_ofPred_eq, mem_sdiff, mem_singleton_iff, inv_eq_zero, hx, not_false_eq_true,
      and_true]
    refine (inv_le_comm₀ ?_ ?_).mp <;>
    simp [zero_lt_iff, hg, hx]

Goal state after:
case refine_2
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ ∀ a ∈ {x | g⁻¹ ≤ x}, ∀ b ∈ {x | g⁻¹ ≤ x}, a < b → Function.onFun (fun x1 x2 ↦ x1 > x2) (fun x ↦ x⁻¹) a b

case refine_3
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ MapsTo (fun x ↦ x⁻¹) ({x | x ≤ g} \ {0}) {x | g⁻¹ ≤ x}

case refine_4
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ∀ a ∈ {x | x ≤ g} \ {0}, ∀ b ∈ {x | x ≤ g} \ {0}, a > b → Function.onFun (fun x1 x2 ↦ x1 < x2) (fun x ↦ x⁻¹) a b
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (coeff (n + 1)) (X * φ) = (coeff n) φ

Tactic:
simp only [coeff, Finsupp.single_add, add_comm n 1]
  convert! φ.coeff_add_monomial_mul (single () 1) (single () n) _
  rw [one_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) (φ * X ^ k) = (coeff n) (ψ * X ^ k)
n : ℕ
⊢ (coeff n) φ = (coeff n) ψ

Tactic:
simpa using h (n + k)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) (X ^ k * φ) = (coeff n) (X ^ k * ψ)
n : ℕ
⊢ (coeff n) φ = (coeff n) ψ

Tactic:
simpa using h (n + k)

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x * y})).factors))) =
    (if x = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors))) *
      if y = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors))

Tactic:
rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← exp_add,
        ← Ideal.span_singleton_mul_span_singleton, ← Associates.mk_mul_mk, ← neg_add,
        Associates.count_mul (Associates.mk_ne_zero'.mpr hx) (Associates.mk_ne_zero'.mpr hy)
          v.associates_irreducible,
        Nat.cast_add]

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

Goal state before:
pp: case succ
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
ih : X s ^ n = (monomial (single s n)) 1
⊢ X s ^ (n + 1) = (monomial (single s (n + 1))) 1

Tactic:
rw [pow_succ, ih, Finsupp.single_add, X, monomial_mul_monomial, one_mul]

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
⊢ ∏ i ∈ range n, (coeff (k i)) f = 0

Tactic:
have hs'' (i : ℕ) (hi : i ∈ s) : k i = 0 := by
    simp only [hs_def, mem_filter] at hi
    rw [hi.2]

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
⊢ ∏ i ∈ range n, (coeff (k i)) f = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R[X]
h : ↑x = ↑y
n✝ : ℕ
⊢ x.coeff n✝ = y.coeff n✝

Tactic:
← coeff_coe,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R[X]
h : ↑x = ↑y
n✝ : ℕ
⊢ (PowerSeries.coeff n✝) ↑x = (PowerSeries.coeff n✝) ↑y
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
⊢ #(range n \ {i ∈ range n | k i = 0}) ≤ degree (∑ x ∈ range n \ s, k x)

Tactic:
rw [← hs_def]

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
⊢ #(range n \ s) ≤ degree (∑ x ∈ range n \ s, k x)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x y : MvPolynomial σ R
h : ↑x = ↑y
m✝ : σ →₀ ℕ
⊢ coeff m✝ x = coeff m✝ y

Tactic:
← coeff_coe,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x y : MvPolynomial σ R
h : ↑x = ↑y
m✝ : σ →₀ ℕ
⊢ (MvPowerSeries.coeff m✝) ↑x = (MvPowerSeries.coeff m✝) ↑y