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

Goal state before:
pp: case even.right
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 := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ : (W.preΨ' (m + 1)).natDegree ≤ expDegree (m + 1) ∧ (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) = ↑(expCoeff (m + 1))
h₂ : (W.preΨ' (m + 2)).natDegree ≤ expDegree (m + 2) ∧ (W.preΨ' (m + 2)).coeff (expDegree (m + 2)) = ↑(expCoeff (m + 2))
h₃ : (W.preΨ' (m + 3)).natDegree ≤ expDegree (m + 3) ∧ (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) = ↑(expCoeff (m + 3))
h₄ : (W.preΨ' (m + 4)).natDegree ≤ expDegree (m + 4) ∧ (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) = ↑(expCoeff (m + 4))
h₅ : (W.preΨ' (m + 5)).natDegree ≤ expDegree (m + 5) ∧ (W.preΨ' (m + 5)).coeff (expDegree (m + 5)) = ↑(expCoeff (m + 5))
⊢ (W.preΨ' (2 * (m + 3))).coeff (expDegree (2 * (m + 3))) = ↑(expCoeff (2 * (m + 3)))

Tactic:
preΨ'_even,

Goal state after:
case even.right
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
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m :=
  fun {m n} {p} ↦ coeff_pow_of_natDegree_le
m : ℕ
h₁ : (W.preΨ' (m + 1)).natDegree ≤ expDegree (m + 1) ∧ (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) = ↑(expCoeff (m + 1))
h₂ : (W.preΨ' (m + 2)).natDegree ≤ expDegree (m + 2) ∧ (W.preΨ' (m + 2)).coeff (expDegree (m + 2)) = ↑(expCoeff (m + 2))
h₃ : (W.preΨ' (m + 3)).natDegree ≤ expDegree (m + 3) ∧ (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) = ↑(expCoeff (m + 3))
h₄ : (W.preΨ' (m + 4)).natDegree ≤ expDegree (m + 4) ∧ (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) = ↑(expCoeff (m + 4))
h₅ : (W.preΨ' (m + 5)).natDegree ≤ expDegree (m + 5) ∧ (W.preΨ' (m + 5)).coeff (expDegree (m + 5)) = ↑(expCoeff (m + 5))
⊢ (W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) -
          W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2).coeff
      (expDegree (2 * (m + 3))) =
    ↑(expCoeff (2 * (m + 3)))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : u ^ 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
⊢ u ^ 4 = E.a₄ / E'.a₄

Tactic:
pow_mul u 2 2,

Goal state after:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : u ^ 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
⊢ (u ^ 2) ^ 2 = E.a₄ / E'.a₄
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.dblZ P = 0

Tactic:
by
  rw [dblZ, hPz, zero_mul]

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

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.negAddY P (W'.neg P) + -2 * P z ^ 3 * (P y - W'.negY P) * 0 -
      (W'.dblZ P ^ 3 +
        -2 * P z ^ 3 * (P y - W'.negY P) *
          (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 [negAddY, neg_X, neg_Y, neg_Z, dblZ, negY]

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ -P y * P x ^ 3 * P z ^ 3 + 2 * P y * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) ^ 2 * P z ^ 3 -
                                            3 * P x ^ 2 * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 2 *
                                              P z +
                                          3 * P x * P y * P x ^ 2 * P z * P z ^ 2 +
                                        P x ^ 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 3 -
                                      2 * P y ^ 2 * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 3 +
                                    W'.a₁ * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) ^ 2 * P z ^ 4 +
                                  W'.a₁ * P y * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 3 * P z -
                                W'.a₁ * P x * P y * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z * P z ^ 3 -
                              W'.a₁ * P y ^ 2 * P x * P z ^ 4 -
                            2 * W'.a₂ * P x * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 4 * P z +
                          2 * W'.a₂ * P x * P y * P x * P z * P z ^ 4 +
                        W'.a₃ * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) ^ 2 * P z ^ 6 -
                      W'.a₃ * P y ^ 2 * P z ^ 6 -
                    W'.a₄ * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 6 * P z -
                  W'.a₄ * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 4 * P z ^ 3 +
                W'.a₄ * P y * P x * P z ^ 3 * P z ^ 4 +
              W'.a₄ * P x * P y * P z * P z ^ 6 -
            2 * W'.a₆ * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 6 * P z ^ 3 +
          2 * W'.a₆ * P y * P z ^ 3 * P z ^ 6 +
        -2 * P z ^ 3 * (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)) * 0 -
      ((P z * (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3))) ^ 3 +
        -2 * P z ^ 3 * (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)) *
          (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.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := hB.topology
⊢ IsOpen[hB.topology] (B i).toAddSubgroup.carrier

Tactic:
let := hB.topology
      rw [isOpen_iff_mem_nhds]
      intro a a_in
      rw [(hB.toModuleFilterBasis.toAddGroupFilterBasis.nhds_hasBasis a).mem_iff]
      use B i
      constructor
      · use i
      · rintro - ⟨b, b_in, rfl⟩
        exact (B i).add_mem a_in b_in

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

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

Tactic:
apply ValueGroupWithZero.sound

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

case h₂
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
⊢ y * w * ↑(s * v) ≤ᵥ x * z * ↑(t * u)
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
Hx : v x = 0
y : R
a✝ : y ∈ ↑(v.ltAddSubgroup ((Units.map ↑embedding) 1))
⊢ v (x * y) < ↑((Units.map ↑embedding) γ)

Tactic:
Valuation.map_mul,

Goal state after:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
Hx : v x = 0
y : R
a✝ : y ∈ ↑(v.ltAddSubgroup ((Units.map ↑embedding) 1))
⊢ v x * v y < ↑((Units.map ↑embedding) γ)
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
γx : Γ₀ˣ
Hx : v x = ↑γx
u : (ofClass v).ValueGroup₀ˣ := ⋯
hu_def : u = Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu : embedding ↑u⁻¹ = ↑γx⁻¹
⊢ ↑(v.ltAddSubgroup ((Units.map ↑embedding) (u⁻¹ * γ))) ⊆
    (fun x_1 ↦ x * x_1) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))

Tactic:
rintro y (vy_lt : v y < ValueGroup₀.embedding (u⁻¹ * γ).1)

Goal state after:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
γx : Γ₀ˣ
Hx : v x = ↑γx
u : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu_def : u = Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu : embedding ↑u⁻¹ = ↑γx⁻¹
y : R
vy_lt : v y < embedding ↑(u⁻¹ * γ)
⊢ y ∈ (fun x_1 ↦ x * x_1) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
γx : Γ₀ˣ
Hx : v x = ↑γx
u : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu_def : u = Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu : embedding ↑u⁻¹ = ↑γx⁻¹
y : R
vy_lt : v y < embedding ↑(u⁻¹ * γ)
⊢ v (x * y) < ↑((Units.map ↑embedding) γ)

Tactic:
Valuation.map_mul,

Goal state after:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
γx : Γ₀ˣ
Hx : v x = ↑γx
u : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu_def : u = Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu : embedding ↑u⁻¹ = ↑γx⁻¹
y : R
vy_lt : v y < embedding ↑(u⁻¹ * γ)
⊢ v x * v y < ↑((Units.map ↑embedding) γ)
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
γx : Γ₀ˣ
Hx : v x = ↑γx
u : (ofClass v).ValueGroup₀ˣ := ⋯
hu_def : u = Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu : embedding ↑u⁻¹ = ↑γx⁻¹
⊢ ↑(v.ltAddSubgroup ((Units.map ↑embedding) (u⁻¹ * γ))) ⊆
    (fun x_1 ↦ x_1 * x) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))

Tactic:
rintro y (vy_lt : v y < ValueGroup₀.embedding (u⁻¹ * γ).1)

Goal state after:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
γx : Γ₀ˣ
Hx : v x = ↑γx
u : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu_def : u = Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu : embedding ↑u⁻¹ = ↑γx⁻¹
y : R
vy_lt : v y < embedding ↑(u⁻¹ * γ)
⊢ y ∈ (fun x_1 ↦ x_1 * x) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ (Filter.comap (fun x ↦ x.2 - x.1) (𝓝 0)).HasBasis (fun x ↦ True) fun γ ↦ {p | v.restrict (p.2 - p.1) < ↑γ}

Tactic:
exact (hasBasis_nhds_zero R Γ₀).comap _

Goal state after:
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⟩

Tactic:
absurd hx
      apply vle_mul_cancel t.prop
      simpa using vle_trans h₁ (mul_vle_mul_left hy s)

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

Goal state before:
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
⊢ ValueGroupWithZero.mk ↑s ⟨x, hx⟩ = ValueGroupWithZero.mk ↑t ⟨y, hy⟩

Tactic:
apply ValueGroupWithZero.sound

Goal state after:
case neg.h₁
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
⊢ ↑s * ↑⟨y, hy⟩ ≤ᵥ ↑t * ↑⟨x, hx⟩

case h₂
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
⊢ ↑t * ↑⟨x, hx⟩ ≤ᵥ ↑s * ↑⟨y, hy⟩
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst✝² : IsUniformAddGroup R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
F : Filter R
⊢ Cauchy F ↔ F.NeBot ∧ ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ

Tactic:
by
  rw [v.toUniformSpace_eq, AddGroupFilterBasis.cauchy_iff]
  apply and_congr Iff.rfl
  simp_rw [v.subgroups_basis.mem_addGroupFilterBasis_iff]
  constructor
  · intro h γ
    simp_rw [restrict_lt_iff_lt_embedding]
    exact h _ (v.subgroups_basis.mem_addGroupFilterBasis γ)
  · rintro h - ⟨γ, rfl⟩
    simp_rw [restrict_lt_iff_lt_embedding] at h
    exact h γ

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
K : Subfield L
F : Filter ↥K
F_cau : Cauchy F
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := K.subtype
hi : IsUniformInducing ⇑i
⊢ Cauchy (map (fun x ↦ x⁻¹) F)

Tactic:
← hi.cauchy_map_iff

Goal state after:
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
F : Filter ↥K
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := K.subtype
F_cau : Cauchy (map (⇑i) F)
hi : IsUniformInducing ⇑i
⊢ Cauchy (map (⇑i) (map (fun x ↦ x⁻¹) F))
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 : Fin 3 → A
⊢ (W'⁄B).dblZ (⇑↑f ∘ P) = ↑f ((W'⁄A).dblZ P)

Tactic:
← map_dblZ,

Goal state after:
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 : Fin 3 → A
⊢ (W'⁄B).dblZ (⇑↑f ∘ P) = ((W'⁄A).map ↑f).dblZ (⇑↑f ∘ P)
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
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
⊢ Valued.v.restrict ((equiv v) r) / Valued.v.restrict ((equiv v) s) ≠ 0

Tactic:
by
    simp only [equiv_apply, restrict_def, ne_eq, div_eq_zero_iff, restrict₀_eq_zero_iff, hv,
      MonoidWithZeroHom.coe_ofClass, not_or, (eq_zero h (r := r.ofVal)).ne,
      (eq_zero h (r := s.ofVal)).ne]
    exact ⟨hr₀.ne', hs₀.ne'⟩

Goal state after:
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:
Valuation.map_mul,

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) *
      (valuation K (maximalIdeal A)) ((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.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) (π ^ 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:
Valuation.map_mul,

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) (π ^ n) * ((algebraMap A K) (π ^ m))⁻¹) *
      (valuation K (maximalIdeal A)) ((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.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
x : (ofClass Valued.v).ValueGroup₀ˣ
u : ↥(ofClass Valued.v).valueGroup := WithZero.unzero ⋯
a : R
ha : (ofClass Valued.v) a ≠ 0
y : R
hu : (ofClass Valued.v) a * ↑↑u = (ofClass Valued.v) y
y₀ : (ofClass Valued.v).ValueGroup₀ := h_val.orderMonoidIso ↑x
hy₀_def : y₀ = h_val.orderMonoidIso ↑x
⊢ y₀ ≠ 0

Tactic:
simp [hy₀_def]

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

Goal state before:
pp: K : Type u_7
inst✝¹ : DivisionRing K
Γ₀ : Type u_8
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
γ : (ofClass v).ValueGroup₀ˣ
r : K
hr : (restrict₀ (ofClass v)) r = ↑γ
⊢ 0 < v r ∧ 0 < v 1 ∧ v.restrict r / v.restrict 1 = ↑γ

Tactic:
simp only [map_one, zero_lt_one, restrict_def, hr, div_one, and_self, and_true]
    rw [← map_zero v]
    simpa [← hr] using embedding_strictMono (WithZero.pos_iff_ne_zero.mpr (Units.ne_zero γ))

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

Goal state before:
pp: case hp
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀'
K : Type u_7
inst✝ : Field K
v : Valuation K Γ₀
w : Valuation K Γ₀'
h : v.IsEquiv w
⊢ IsClosed {a | Valued.v a ≤ 1 ↔ Valued.v ((mapEquiv h.uniformEquiv) a) ≤ 1}

Tactic:
have h1 (x : UniformSpace.Completion (WithVal v)) :
      Valued.v x ≤ 1 ↔ Valued.v.restrict x ≤ 1 := by rw [restrict_le_one_iff]
    simp_rw [h1]
    convert!
      (mapEquiv h.uniformEquiv).toHomeomorph.isClosed_setOfPred_iff
        (Valued.isClopen_closedBall _ one_ne_zero) (Valued.isClopen_closedBall _ one_ne_zero)
    rw [restrict_le_one_iff]
    rfl

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: e : ℤ ≃+ ℤ
this : e 1 = 1 ∨ -e 1 = 1
⊢ e = AddEquiv.refl ℤ ∨ e = AddEquiv.neg ℤ

Tactic:
by simpa [AddEquiv.ext_int_iff, neg_eq_iff_eq_neg]

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✝ : Archimedean G
H : ∀ (x : G), ¬IsLeast {y | 0 < y} x
⊢ ∀ (a₁ a₂ : G), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
intro x y hxy

Goal state after:
case neg
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
H : ∀ (x : G), ¬IsLeast {y | 0 < y} x
x y : G
hxy : x < y
⊢ ∃ a, x < a ∧ a < y
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (⇑embedding ∘ extension) (x * y) = (⇑embedding ∘ extension) x * (⇑embedding ∘ extension) y

Tactic:
simp only [Function.comp_apply, ← map_mul]
    rw [embedding_strictMono.injective.eq_iff]
    apply Completion.induction_on₂ x y
      (p := fun x y => extension (x * y) = extension x * extension y)
    · have c1 : Continuous fun x : hat K × hat K => Valued.extension (x.1 * x.2) :=
        Valued.continuous_extension.comp (continuous_fst.mul continuous_snd)
      have c2 : Continuous fun x : hat K × hat K => Valued.extension x.1 * Valued.extension x.2 :=
        (Valued.continuous_extension.comp continuous_fst).mul
          (Valued.continuous_extension.comp continuous_snd)
      exact isClosed_eq c1 c2
    · intro x y
      norm_cast
      exact Valuation.map_mul _ _ _

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : PartialOrder α
inst✝² : CommMonoid β
inst✝¹ : PartialOrder β
e : α ≃*o β
inst✝ : MulArchimedean α
⊢ ∀ (x : β) {y : β}, 1 < y → ∃ n, x ≤ y ^ n

Tactic:
intro x y hxy

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : PartialOrder α
inst✝² : CommMonoid β
inst✝¹ : PartialOrder β
e : α ≃*o β
inst✝ : MulArchimedean α
x y : β
hxy : 1 < y
⊢ ∃ n, x ≤ y ^ n