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

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
inst✝⁴ : IsCofiltered I
R : CommRingCat
inst✝³ : IsAffine (Spec R)
S : CommRingCat
inst✝² : IsAffine (Spec S)
φ : R ⟶ S
inst✝¹ : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst✝ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
t : D ⋙ Scheme.Spec ⟶ (Functor.const I).obj (Spec R)
a : c.pt ⟶ Spec S
ha : c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ)
e : ((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec ≅ (Functor.const I).obj (Spec R) :=
  NatIso.ofComponents (fun x ↦ Iso.refl ((((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec).obj x)) ⋯
⊢ t =
    Functor.whiskerRight { app := fun i ↦ Spec.preimage (t.app (Opposite.unop i)), naturality := ⋯ }.rightOp
        Scheme.Spec ≫
      e.hom

Tactic:
ext : 2; simp [e]

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

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K
inst✝¹³ : Field L
W' : Affine R
W : Affine F
inst✝¹² : DecidableEq F
inst✝¹¹ : DecidableEq K
inst✝¹⁰ : DecidableEq L
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
⊢ ∀ (x y : (W'⁄F).Point),
    (match x + y with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯) =
      (match x with
        | zero => 0
        | some x y h => some (f x) (f y) ⋯) +
        match y with
        | zero => 0
        | some x y h => some (f x) (f y) ⋯

Tactic:
rintro (_ | ⟨x₁, y₁, h₁⟩) (_ | ⟨x₂, y₂, h₂⟩)
    any_goals rfl
    by_cases hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂
    · rw [add_of_Y_eq hxy.left hxy.right,
        add_of_Y_eq (congr_arg _ hxy.left) <| by rw [hxy.right, baseChange_negY]]
    · simpa only [add_some hxy, ← baseChange_addX, ← baseChange_addY, ← baseChange_slope] using!
        (add_some fun h ↦ hxy ⟨f.injective h.1, f.injective (W'.baseChange_negY f .. ▸ h).2⟩).symm

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
h : ↑n ≠ 0
⊢ (W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) ≠ 0

Tactic:
by
  induction n using Int.negInduction with
  | nat n => simpa only [preΨ_ofNat, Int.even_coe_nat]
      using! W.coeff_preΨ'_ne_zero <| by exact_mod_cast h
  | neg ih n => simpa only [preΨ_neg, coeff_neg, neg_ne_zero, Int.natAbs_neg, even_neg]
        using! ih n <| neg_ne_zero.mp <| by exact_mod_cast h

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

Goal state before:
pp: case succ.succ.left
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) := ⋯
n : ℕ
hd : (n + 1 + 1) ^ 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : (n + 1 + 1) ^ 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ ((X * W.preΨ' (n + 1 + 1) ^ 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
        W.preΨ' (n + 1 + 2) * W.preΨ' (n + 1) * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
    (n + 1 + 1) ^ 2

Tactic:
← max_self <| (_ + _) ^ 2,

Goal state after:
case succ.succ.left
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1 + 1) ^ 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : (n + 1 + 1) ^ 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ ((X * W.preΨ' (n + 1 + 1) ^ 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
        W.preΨ' (n + 1 + 2) * W.preΨ' (n + 1) * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
    max ((n + 1 + 1) ^ 2) ((n + 1 + 1) ^ 2)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ ![P x, -P y, 0] = ![P y ^ 2 / P x ^ 2 * ![1, 1, 0] x, (-(P y / P x)) ^ 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]

Tactic:
(equation_of_Z_eq_zero hPz).mp hP.left,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ ![P x, -P y, 0] = ![P x ^ 3 / P x ^ 2 * ![1, 1, 0] x, (-(P y / P x)) ^ 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ ![P x, -P y, 0] = ![P x, -(P y ^ 2 * P y / P x ^ 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]

Tactic:
(equation_of_Z_eq_zero hPz).mp hP.left,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ ![P x, -P y, 0] = ![P x, -(P x ^ 3 * P y / P x ^ 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
⊢ W.Nonsingular (W.add P Q)

Tactic:
by
  by_cases hPz : P z = 0
  · by_cases hQz : Q z = 0
    · simp only [add_of_Z_eq_zero hP hQ hPz hQz,
        nonsingular_smul _ <| (isUnit_X_of_Z_eq_zero hP hPz).pow 2, nonsingular_zero]
    · simpa only [add_of_Z_eq_zero_left hP.left hPz hQz,
        nonsingular_smul _ <| (isUnit_X_of_Z_eq_zero hP hPz).mul <| Ne.isUnit hQz]
  · by_cases hQz : Q z = 0
    · simpa only [add_of_Z_eq_zero_right hQ.left hPz hQz,
        nonsingular_smul _ ((isUnit_X_of_Z_eq_zero hQ hQz).mul <| Ne.isUnit hPz).neg]
    · by_cases hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
      · by_cases hy : P y * Q z ^ 3 = Q y * P z ^ 3
        · simp only [add_of_Y_eq hPz hQz hxy.left hy hxy.right, nonsingular_smul _ <|
              isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, nonsingular_zero]
        · simp only [add_of_Y_ne hP.left hQ.left hPz hQz hxy.left hy,
            nonsingular_smul _ <| isUnit_addU_of_Y_ne hPz hQz hy, nonsingular_zero]
      · classical
        have := nonsingular_add_of_Z_ne_zero hP hQ hPz hQz hxy
        by_cases hx : P x * Q z ^ 2 = Q x * P z ^ 2
        · simpa only [add_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx,
            nonsingular_smul _ <| isUnit_dblZ_of_Y_ne' hP.left hQ.left hPz hx <| not_and.mp hxy hx]
        · simpa only [add_of_X_ne hP.left hQ.left hPz hQz hx,
            nonsingular_smul _ <| isUnit_addZ_of_X_ne hx]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y z : R
⊢ x * y * z =ᵥ x * z * y

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y z : R
⊢ x * (y * z) =ᵥ x * z * y
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]

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ P x * P x ^ 2 * P z ^ 2 - 2 * P y * P y * P z * P z + P x ^ 2 * P x * P z ^ 2 - W'.a₁ * P x * P y * P z ^ 2 * P z -
                      W'.a₁ * P y * P x * P z * P z ^ 2 +
                    2 * W'.a₂ * P x * P x * P z ^ 2 * P z ^ 2 -
                  W'.a₃ * P y * P z ^ 4 * P z -
                W'.a₃ * P y * P z * P z ^ 4 +
              W'.a₄ * P x * P z ^ 4 * P z ^ 2 +
            W'.a₄ * P x * P z ^ 2 * P z ^ 4 +
          2 * W'.a₆ * P z ^ 4 * P z ^ 4 +
        -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
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: 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
x✝¹ x✝ : W.Point
⊢ x✝¹ + x✝ = x✝ + x✝¹

Tactic:
classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, add_comm]

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 : R
⊢ ∀ (x y z w : R) (t s u v : ↥(posSubmonoid R)),
    x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → z * ↑u ≤ᵥ w * ↑v → w * ↑v ≤ᵥ z * ↑u → (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)

Tactic:
intro x y z w t s u v h₁ h₂ h₃ h₄
    by_cases hw : w ≤ᵥ 0 <;> by_cases hz : z ≤ᵥ 0
    · refine propext ⟨fun h => vle_trans ?_ (zero_vle _), fun h => vle_trans ?_ (zero_vle _)⟩
      · apply vle_mul_cancel (s * v).prop
        grw [veq_mul_right_comm, Submonoid.coe_mul, ← mul_assoc]
        apply (mul_vle_mul_left (mul_vle_mul_left h₂ v) u).trans
        grw [veq_mul_right_comm x]
        apply (mul_vle_mul_left (mul_vle_mul_left h t) u).trans
        apply vle_trans (mul_vle_mul_left (mul_vle_mul_left (mul_vle_mul_left hz s) t) u)
        simp
      · apply vle_mul_cancel (t * u).prop
        grw [veq_mul_right_comm, Submonoid.coe_mul, ← mul_assoc]
        apply (mul_vle_mul_left (mul_vle_mul_left h₁ u) v).trans
        grw [veq_mul_right_comm y]
        apply (mul_vle_mul_left (mul_vle_mul_left h s) v).trans
        apply vle_trans (mul_vle_mul_left (mul_vle_mul_left (mul_vle_mul_left hw t) s) v)
        simp
    · absurd hz
      apply vle_mul_cancel u.prop
      simpa using h₃.trans (mul_vle_mul_left hw v)
    · absurd hw
      apply vle_mul_cancel v.prop
      simpa using h₄.trans (mul_vle_mul_left hz u)
    · refine propext ⟨fun h => ?_, fun h => ?_⟩
      · apply vle_mul_cancel s.prop
        apply vle_mul_cancel hz
        calc y * u * s * z
          _ =ᵥ y * s * (z * u) := by grw [veq_mul_comm z, veq_mul_mul_mul_comm, mul_assoc]
          _ ≤ᵥ x * t * (w * v) := by gcongr
          _ =ᵥ x * v * (t * w) := by grw [veq_mul_comm w, veq_mul_mul_mul_comm, mul_assoc]
          _ ≤ᵥ z * s * (t * w) := by gcongr
          _ =ᵥ w * t * s * z := by grw [veq_mul_comm, veq_mul_comm _ w, veq_mul_comm z, ← mul_assoc]
      · apply vle_mul_cancel t.prop
        apply vle_mul_cancel hw
        calc x * v * t * w
          _ =ᵥ x * t * (w * v) := by grw [veq_mul_comm w, veq_mul_mul_mul_comm, mul_assoc]
          _ ≤ᵥ y * s * (z * u) := by gcongr
          _ =ᵥ y * u * (s * z) := by grw [veq_mul_comm z, veq_mul_mul_mul_comm, mul_assoc]
          _ ≤ᵥ w * t * (s * z) := by gcongr
          _ =ᵥ z * s * t * w := by grw [veq_mul_comm, veq_mul_comm _ z, veq_mul_comm w, ← mul_assoc]

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

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

Tactic:
induction b using ValueGroupWithZero.ind with | 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.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: K : Type u
inst✝³ : DivisionRing K
Γ₀ : Type v
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : MulArchimedean Γ₀
inst✝ : Valued K Γ₀
r : Γ₀
hr : r ≠ 0
h : ∀ (x : K), v x ≠ 0 → r < v x
⊢ ∀ (x : K), x ≠ 0 → v x = 1

Tactic:
simpa using Valued.v.map_eq_one_of_forall_lt hr h

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
x : R
hx : x ∈ {x | v.restrict x < r}
⊢ ∃ γ, {y | v.restrict (y - x) < ↑γ} ⊆ {x | v.restrict x < r}

Tactic:
simp only [ofPred_subset_ofPred]

Goal state after:
case inr
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
x : R
hx : x ∈ {x | v.restrict x < r}
⊢ ∃ γ, ∀ (a : R), v.restrict (a - x) < ↑γ → v.restrict a < r
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
x : R
hx : x ∈ {x | v.restrict x ≤ r}
⊢ ∃ γ, {y | v.restrict (y - x) < ↑γ} ⊆ {x | v.restrict x ≤ r}

Tactic:
simp only [ofPred_subset_ofPred]

Goal state after:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
x : R
hx : x ∈ {x | v.restrict x ≤ r}
⊢ ∃ γ, ∀ (a : R), v.restrict (a - x) < ↑γ → v.restrict a ≤ r
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ Nontrivial (ValueGroupWithZero R)ˣ → IsNontrivial R

Tactic:
rintro ⟨r, s, h⟩

Goal state after:
case mpr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
r s : (ValueGroupWithZero R)ˣ
h : r ≠ s
⊢ IsNontrivial R
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case inr
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
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
x : R
hx : x ∈ {x | v.restrict x < r}
⊢ ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ {x | v.restrict x < r}

Tactic:
simp only [ofPred_subset_ofPred]

Goal state after:
case inr
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
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
x : R
hx : x ∈ {x | v.restrict x < r}
⊢ ∃ γ, ∀ (a : R), v.restrict (a - x) < ↑γ → v.restrict a < r
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
⊢ (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹

Tactic:
simp [Function.comp_def]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x y v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I ↑(span {v * x}) = span {y}
z : R
hi : z * y * x ∈ I
⊢ z * (x * y) = z * y * x

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x y v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I ↑(span {v * x}) = span {y}
z : R
hi : z * y * x ∈ I
⊢ z * (x * y) = z * (y * x)
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
h1 : ∀ (x : A), v x ≠ 0 → v x = 1
y : Γˣ
x : A
⊢ (MonoidWithZeroHom.ofClass v) x = ↑y → ↑y = ↑1

Tactic:
specialize h1 x

Goal state after:
Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝¹ : Ring A
v : Valuation A Γ
inst✝ : v.IsRankOneDiscrete
y : Γˣ
x : A
h1 : v x ≠ 0 → v x = 1
⊢ (MonoidWithZeroHom.ofClass v) x = ↑y → ↑y = ↑1
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 Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer 0
h0 : π = 0
⊢ False

Tactic:
IsUniformizer,

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝ : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v 0 = ↑(IsRankOneDiscrete.generator v)
h0 : π = 0
⊢ False
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq 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
hZ : ∀ {n : ℕ}, IsUnit (addZ P Q ^ n)
⊢ ![W.addX P Q, W.addY P Q, addZ P Q] =
    ![W.addX P Q,
      addZ P Q ^ 3 *
        ![W.addX P Q / addZ P Q ^ 2,
            W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
              (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
            1]
          y,
      addZ P Q *
        ![W.addX P Q / addZ P Q ^ 2,
            W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
              (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
            1]
          z]

Tactic:
← addY_of_Z_ne_zero hP hQ hPz hQz hx,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq 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
hZ : ∀ {n : ℕ}, IsUnit (addZ P Q ^ n)
⊢ ![W.addX P Q, W.addY P Q, addZ P Q] =
    ![W.addX P Q, addZ P Q ^ 3 * ![W.addX P Q / addZ P Q ^ 2, W.addY P Q / addZ P Q ^ 3, 1] y,
      addZ P Q * ![W.addX P Q / addZ P Q ^ 2, W.addY P Q / addZ P Q ^ 3, 1] z]
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
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : R
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
⊢ Valued.v.restrict ((equiv v).symm r) / Valued.v.restrict ((equiv v).symm s) ≠ 0

Tactic:
simp [Valuation.restrict_def, restrict₀_eq_zero_iff, (eq_zero h (r := r)).ne, ← hv,
      (eq_zero h (r := s)).ne, hr₀.ne', hs₀.ne']

Goal state after:
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₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hx_mem : π.val ^ n ∈ P
hu : x = π.val ^ n * ↑u
hn : ¬n = 0
⊢ Submodule.IsPrincipal P

Tactic:
IsPrime.pow_mem_iff_mem hP _ (pos_iff_ne_zero.mpr hn),

Goal state after:
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₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hx_mem : π.val ∈ P
hu : x = π.val ^ n * ↑u
hn : ¬n = 0
⊢ Submodule.IsPrincipal P
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case neg
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 :
  (valuation K (maximalIdeal A))
      ((algebraMap A K) ↑u * (algebraMap A K) (π ^ n) * ((algebraMap A K) (π ^ m) * (algebraMap A K) ↑w)⁻¹) ≤
    1
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
⊢ ∃ a, (algebraMap A K) a = x

Tactic:
mul_assoc,

Goal state after:
case neg
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 :
  (valuation K (maximalIdeal A))
      ((algebraMap A K) ↑u * ((algebraMap A K) (π ^ n) * ((algebraMap A K) (π ^ m) * (algebraMap A K) ↑w)⁻¹)) ≤
    1
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
⊢ ∃ a, (algebraMap A K) a = x
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)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v x = v y
x_ne : x ≠ 0
⊢ x⁻¹ - y⁻¹ = x⁻¹ * y * y⁻¹ - x⁻¹ * x * y⁻¹

Tactic:
mul_assoc,

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)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v x = v y
x_ne : x ≠ 0
⊢ x⁻¹ - y⁻¹ = x⁻¹ * (y * y⁻¹) - x⁻¹ * x * y⁻¹
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)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v x = v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ (v x)⁻¹ * v (y - x) * (v y)⁻¹ = v (y - x) * (v y * v y)⁻¹

Tactic:
mul_assoc,

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)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v x = v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ (v x)⁻¹ * (v (y - x) * (v y)⁻¹) = v (y - x) * (v y * v y)⁻¹