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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 2 ≠ 0
⊢ W.preΨ₄.coeff 6 ≠ 0

Tactic:
by
  rwa [coeff_preΨ₄]

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (W.map f).ψ n = Polynomial.map (mapRingHom f) (W.ψ n)

Tactic:
rw [← coe_mapRingHom]
  simp [ψ]

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

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

Tactic:
rw [← map_Φ, map_baseChange]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ W.c₄ = 1

Tactic:
rw [c₄_of_isCharTwoJNeZeroNF, b₂_of_isCharTwoJNeZeroNF_of_char_two]
  ring1

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.IsCharTwoJEqZeroNF
inst✝ : CharP F 2
⊢ W.j = 0

Tactic:
rw [j, c₄_of_isCharTwoJEqZeroNF_of_char_two]

Goal state after:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharTwoJEqZeroNF
inst✝ : CharP F 2
⊢ ↑W.Δ'⁻¹ * 0 ^ 3 = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case pos
F : Type u_1
inst✝³ : Field F
inst✝² : IsSepClosed F
E E' : WeierstrassCurve F
inst✝¹ : E.IsElliptic
inst✝ : E'.IsElliptic
heq : E.j = E'.j
h✝ : CharP F 2
⊢ ∃ C, C • E = E'

Tactic:
exact exists_variableChange_of_char_two _ _ heq

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

Goal state before:
pp: A : Type u_3
ι : Type u_4
inst✝ : CommRing A
B : ι → AddSubgroup A
inter : ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
mul : ∀ (i : ι), ∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)
leftMul : ∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun y ↦ x * y) ⁻¹' ↑(B i)
x : A
i j : ι
hj : ↑(B j) ⊆ (fun y ↦ x * y) ⁻¹' ↑(B i)
⊢ ↑(B j) ⊆ (fun x_1 ↦ x_1 * x) ⁻¹' ↑(B i)

Tactic:
by simpa only [mul_comm] using hj

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

Goal state before:
pp: case mp
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
⊢ (∃ i ∈ hB.toRingFilterBasis.toAddGroupFilterBasis, id i ⊆ s) → ∃ i, True ∧ ↑(B i) ⊆ s

Tactic:
rintro ⟨-, ⟨i, rfl⟩, hi⟩
      exact ⟨i, trivial, hi⟩

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
⊢ toAffine W (u • P) = toAffine W P

Tactic:
by_cases hP : W.Nonsingular P
  · by_cases hPz : P z = 0
    · rw [toAffine_of_Z_eq_zero <| mul_eq_zero_of_right u hPz, toAffine_of_Z_eq_zero hPz]
    · rw [toAffine_of_Z_ne_zero ((nonsingular_smul P hu).mpr hP) <| mul_ne_zero hu.ne_zero hPz,
        toAffine_of_Z_ne_zero hP hPz, Affine.Point.some.injEq]
      simp only [smul_fin3_ext, mul_pow, mul_div_mul_left _ _ (hu.pow _).ne_zero, and_self]
  · rw [toAffine_of_singular <| hP.comp (nonsingular_smul P hu).mp, toAffine_of_singular hP]

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

Goal state before:
pp: case inr.inl
K : Type u
inst✝² : DivisionRing K
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : MulArchimedean Γ₀
v : Valuation K Γ₀
x : K
hx : v x ≠ 0
r : Γ₀ˣ
hr : ↑r ≠ 0
h : ∀ (x : K), v x ≠ 0 → ↑r < v x
H : Units.mk0 (v x) hx = 1
⊢ v x = 1

Tactic:
simpa [Units.ext_iff] using H

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

Goal state before:
pp: case left
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : r * ↑v ≤ᵥ s * ↑u
h2 : s * ↑u ≤ᵥ r * ↑v
h3 : s * ↑w ≤ᵥ t * ↑v
h4 : t * ↑v ≤ᵥ s * ↑w
⊢ r * ↑w ≤ᵥ t * ↑u

pp: case right
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : r * ↑v ≤ᵥ s * ↑u
h2 : s * ↑u ≤ᵥ r * ↑v
h3 : s * ↑w ≤ᵥ t * ↑v
h4 : t * ↑v ≤ᵥ s * ↑w
⊢ t * ↑u ≤ᵥ r * ↑w

Tactic:
· have := mul_vle_mul h1 (vle_refl ↑w)
        grw [veq_mul_right_comm (x := s)] at this
        have := vle_trans this (mul_vle_mul h3 (vle_refl _))
        grw [veq_mul_right_comm r, veq_mul_right_comm t] at this
        simpa using this

Goal state after:
case right
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : r * ↑v ≤ᵥ s * ↑u
h2 : s * ↑u ≤ᵥ r * ↑v
h3 : s * ↑w ≤ᵥ t * ↑v
h4 : t * ↑v ≤ᵥ s * ↑w
⊢ t * ↑u ≤ᵥ r * ↑w
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)
⊢ x * ↑t ≤ᵥ y * ↑s →
    y * ↑s ≤ᵥ x * ↑t →
      z * ↑u ≤ᵥ w * ↑v →
        w * ↑v ≤ᵥ z * ↑u → ValueGroupWithZero.mk (x * z) (s * v) = ValueGroupWithZero.mk (y * w) (t * u)

Tactic:
h₁

Goal state after:
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
⊢ y * ↑s ≤ᵥ x * ↑t →
    z * ↑u ≤ᵥ w * ↑v → w * ↑v ≤ᵥ z * ↑u → ValueGroupWithZero.mk (x * z) (s * v) = ValueGroupWithZero.mk (y * w) (t * u)
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
n : ℕ
x y : R
t s : ↥(posSubmonoid R)
⊢ x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → ValueGroupWithZero.mk (x ^ n) (s ^ n) = ValueGroupWithZero.mk (y ^ n) (t ^ n)

Tactic:
h₁

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z : R
n : ℕ
x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
⊢ y * ↑s ≤ᵥ x * ↑t → ValueGroupWithZero.mk (x ^ n) (s ^ n) = ValueGroupWithZero.mk (y ^ n) (t ^ n)
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)
⊢ 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:
h₁

Goal state after:
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
⊢ y * ↑s ≤ᵥ x * ↑t → z * ↑u ≤ᵥ w * ↑v → w * ↑v ≤ᵥ z * ↑u → (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)
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
inst✝ : DecidableEq F
⊢ Function.RightInverse fromAffine toAffineLift

Tactic:
rintro (_ | _)

Goal state after:
case zero
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
⊢ (fromAffine Affine.Point.zero).toAffineLift = Affine.Point.zero

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✝
⊢ (fromAffine (Affine.Point.some x✝ y✝ h✝)).toAffineLift = Affine.Point.some x✝ y✝ h✝
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case pos.refine_1
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
hz : z ≤ᵥ 0
h : x * ↑v ≤ᵥ z * ↑s
⊢ x * ↑t * ↑v * ↑u ≤ᵥ 0 * (↑s * ↑v)

Tactic:
veq_mul_right_comm x

Goal state after:
case pos.refine_1
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
hz : z ≤ᵥ 0
h : x * ↑v ≤ᵥ z * ↑s
⊢ x * ↑v * ↑t * ↑u ≤ᵥ 0 * (↑s * ↑v)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case pos.refine_1
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
hz : z ≤ᵥ 0
h : x * ↑v ≤ᵥ z * ↑s
⊢ y * ↑u ≤ᵥ 0

Tactic:
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

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 : R
t s : ↥(posSubmonoid R)
⊢ x * ↑t ≤ᵥ y * ↑s →
    y * ↑s ≤ᵥ x * ↑t →
      (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
        if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

Tactic:
h₁

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
⊢ y * ↑s ≤ᵥ x * ↑t →
    (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
      if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : x ≤ᵥ 0
hy : y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

Tactic:
· simp [hx, hy]

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: case mp
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (∀ (U : Set R), (∃ i, U = ↑(v.ltAddSubgroup ((Units.map ↑embedding) i))) → ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) →
    ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ

Tactic:
intro h γ

Goal state after:
case mp
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
h : ∀ (U : Set R), (∃ i, U = ↑(v.ltAddSubgroup ((Units.map ↑embedding) i))) → ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
γ : (ofClass v).ValueGroup₀ˣ
⊢ ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
r : R
s : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk r s = (valuation R) r / (valuation R) ↑s

Tactic:
eq_div_iff (valuation_posSubmonoid_ne_zero _)

Goal state after:
R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
r : R
s : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk r s * (valuation R) ↑s = (valuation R) r
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case mp
R : Type u_1
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst✝² : IsUniformAddGroup R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
F : Filter R
⊢ (∀ (U : Set R), (∃ i, U = ↑(v.ltAddSubgroup ((Units.map ↑embedding) i))) → ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) →
    ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ

Tactic:
intro h γ

Goal state after:
case mp
R : Type u_1
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst✝² : IsUniformAddGroup R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
F : Filter R
h : ∀ (U : Set R), (∃ i, U = ↑(v.ltAddSubgroup ((Units.map ↑embedding) i))) → ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
γ : (ofClass v).ValueGroup₀ˣ
⊢ ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case mk
R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
a : R
b : ↥(posSubmonoid R)
⊢ ∃ a_1 b_1, (valuation R) a_1 / (valuation R) ↑b_1 = ValueGroupWithZero.mk a b

Tactic:
use a, b

Goal state after:
case h
R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
a : R
b : ↥(posSubmonoid R)
⊢ (valuation R) a / (valuation R) ↑b = ValueGroupWithZero.mk a b
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
γ : (ValueGroupWithZero R)ˣ
b a : ↥(posSubmonoid R)
hab : (valuation R) ↑a / (valuation R) ↑b = ↑γ
⊢ ∃ a b, (valuation R) ↑a / (valuation R) ↑b = ↑γ

Tactic:
use a, b

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

Goal state before:
pp: K : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : ValuativeRel K
Γ₀ : Type u_3
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
inst✝³ : TopologicalSpace K
inst✝² : IsValuativeTopology K
inst✝¹ : MulArchimedean Γ₀
v : Valuation K Γ₀
inst✝ : v.Compatible
r : Γ₀
hr : r ≠ 0
h : ∀ (x : K), v x ≠ 0 → r < v x
⊢ ∀ (x : K), x ≠ 0 → v x = 1

Tactic:
by simpa using v.map_eq_one_of_forall_lt hr h

Goal state after:
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
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
⊢ Cauchy (map ((fun y ↦ ↑y) ∘ fun x ↦ x⁻¹) (Filter.comap coe' (𝓝 y)))

Tactic:
← Filter.map_map

Goal state after:
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
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
⊢ Cauchy (map (fun y ↦ ↑y) (map (fun x ↦ x⁻¹) (Filter.comap coe' (𝓝 y))))
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
⊢ Function.Injective fun x ↦ embedding (⋯.orderMonoidIso x)

Tactic:
by rw [← Function.comp_def, EquivLike.injective_comp]
          exact embedding_strictMono.injective

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

Goal state before:
pp: K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : IsTopologicalDivisionRing L
inst✝¹ : T0Space L
inst✝ : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : F = ⊥
this : F.NeBot
hx : F ≤ 𝓝 0
⊢ False

Tactic:
exact cau_F.1.ne hF

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime

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

Tactic:
rw [← mem_span_singleton', ← hy, mem_colon_span_singleton, mul_comm v, ← mul_assoc]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x y u : R
hi : u * x ∈ I
v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I ↑(span {v * x}) = span {y}
⊢ u * x * v ∈ I
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.addXYZ P Q =
    addZ P Q •
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        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]

Tactic:
erw [addXYZ, smul_fin3, ← addX_of_Z_ne_zero hP hQ hPz hQz hx, hZ.mul_div_cancel,
    ← addY_of_Z_ne_zero hP hQ hPz hQz hx, hZ.mul_div_cancel, mul_one]

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

Goal state before:
pp: case pos
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 y : K
h : (valuation K (maximalIdeal A)) x = (valuation K (maximalIdeal A)) y
hx : x = 0
⊢ ∃ u, u • x = y

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 y : K
h : (valuation K (maximalIdeal A)) x = (valuation K (maximalIdeal A)) y
hx : ¬x = 0
⊢ ∃ u, u • x = y

Tactic:
· rw [eq_comm] at h
    simp_all

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 y : K
h : (valuation K (maximalIdeal A)) x = (valuation K (maximalIdeal A)) y
hx : ¬x = 0
⊢ ∃ u, u • x = y
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 y : K
h : (valuation K (maximalIdeal A)) x = (valuation K (maximalIdeal A)) y
hx : ¬x = 0
hy : ¬y = 0
this : y / x ∈ Submonoid.map (algebraMap A K) (IsUnit.submonoid A)
⊢ ∃ u, u • x = y

Tactic:
obtain ⟨u, h⟩ := this

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 y : K
h✝ : (valuation K (maximalIdeal A)) x = (valuation K (maximalIdeal A)) y
hx : ¬x = 0
hy : ¬y = 0
u : A
h : u ∈ ↑(IsUnit.submonoid A) ∧ (algebraMap A K) u = y / x
⊢ ∃ u, u • x = y
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_1
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
⊢ b ∈ {y | y ∈ closure {b} ∧ 1 < y}

pp: case refine_2
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
⊢ b ∈ lowerBounds {y | y ∈ closure {b} ∧ 1 < y}

Tactic:
· simp [h]

Goal state after:
case refine_2
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
⊢ b ∈ lowerBounds {y | y ∈ closure {b} ∧ 1 < y}
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⟩
⊢ False

Tactic:
obtain ⟨w, hw, hw'⟩ := exists_between hz'

Goal state after:
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
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 Γ₀
⊢ (⇑embedding ∘ extension) 0 = 0

Tactic:
by
    rw [Function.comp_apply, map_eq_zero, ← v.restrict.map_zero (R := K),
      ← Valued.extension_extends (0 : K), Completion.coe_zero]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
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
x : G₀
⊢ x ≤ g → ¬x = 0 → g⁻¹ ≤ x⁻¹

Tactic:
intro hxg

Goal state after:
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
x : G₀
hxg : x ≤ g
⊢ ¬x = 0 → g⁻¹ ≤ x⁻¹
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ ⇑(monomial 0) = ⇑C

Tactic:
monomial,

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ ⇑(MvPowerSeries.monomial (single () 0)) = ⇑C
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : x ≠ 0
⊢ v.intValuation x ≤ 1

Tactic:
rw [v.intValuation_if_neg hx, ← exp_zero, exp_le_exp, Right.neg_nonpos_iff]

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : x ≠ 0
⊢ 0 ≤ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)