mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (2 * ↑n + 1) =
      complEDS b c d k ↑n ^ 2 * normEDS b c d ((↑n + 1) * k + 1) * normEDS b c d ((↑n + 1) * k - 1) -
        complEDS b c d k (↑n + 1) ^ 2 * normEDS b c d (↑n * k + 1) * normEDS b c d (↑n * k - 1)
m : ℕ
⊢ complEDS b c d k (2 * -↑(m + 1) + 1) =
    complEDS b c d k (-↑(m + 1)) ^ 2 * normEDS b c d ((-↑(m + 1) + 1) * k + 1) *
        normEDS b c d ((-↑(m + 1) + 1) * k - 1) -
      complEDS b c d k (-↑(m + 1) + 1) ^ 2 * normEDS b c d (-↑(m + 1) * k + 1) * normEDS b c d (-↑(m + 1) * k - 1)

Tactic:
simp_rw [Nat.cast_succ, show 2 * -(m + 1 : ℤ) + 1 = -(2 * m + 1) by rfl,
      show (-(m + 1 : ℤ) + 1) = -m by ring1, neg_mul, ← sub_neg_eq_add, ← neg_sub', sub_neg_eq_add,
      ← neg_add', complEDS_neg, normEDS_neg, ih]

Goal state after:
case neg.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (2 * ↑n + 1) =
      complEDS b c d k ↑n ^ 2 * normEDS b c d ((↑n + 1) * k + 1) * normEDS b c d ((↑n + 1) * k - 1) -
        complEDS b c d k (↑n + 1) ^ 2 * normEDS b c d (↑n * k + 1) * normEDS b c d (↑n * k - 1)
m : ℕ
⊢ -(complEDS b c d k ↑m ^ 2 * normEDS b c d ((↑m + 1) * k + 1) * normEDS b c d ((↑m + 1) * k - 1) -
        complEDS b c d k (↑m + 1) ^ 2 * normEDS b c d (↑m * k + 1) * normEDS b c d (↑m * k - 1)) =
    (-complEDS b c d k (↑m + 1)) ^ 2 * -normEDS b c d (↑m * k - 1) * -normEDS b c d (↑m * k + 1) -
      (-complEDS b c d k ↑m) ^ 2 * -normEDS b c d ((↑m + 1) * k - 1) * -normEDS b c d ((↑m + 1) * k + 1)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ ¬some x₁ y₁ h✝¹ + some x₂ y₂ h✝ = 0

Tactic:
simpa only [add_some hxy] using some_ne_zero _

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (X * 1 ^ 2 * (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆) -
      W.Ψ₃ * W.preΨ' 1 * if Even 1 then C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆ else 1) =
    X ^ 4 - C W.b₄ * X ^ 2 - C (2 * W.b₆) * X - C W.b₈

Tactic:
preΨ'_one,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (X * 1 ^ 2 * (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆) -
      W.Ψ₃ * 1 * if Even 1 then C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆ else 1) =
    X ^ 4 - C W.b₄ * X ^ 2 - C (2 * W.b₆) * X - C W.b₈
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (X * W.preΨ₄ ^ 2 * W.Ψ₂Sq -
      (W.preΨ₄ * 1 ^ 3 * W.Ψ₂Sq ^ 2 - W.preΨ' (0 + 1) * W.preΨ' (0 + 3) ^ 3 * if Even 0 then 1 else W.Ψ₂Sq ^ 2) *
          W.preΨ' 3 *
        if Even 3 then W.Ψ₂Sq else 1) =
    X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)

Tactic:
preΨ'_one,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (X * W.preΨ₄ ^ 2 * W.Ψ₂Sq -
      (W.preΨ₄ * 1 ^ 3 * W.Ψ₂Sq ^ 2 - 1 * W.preΨ' (0 + 3) ^ 3 * if Even 0 then 1 else W.Ψ₂Sq ^ 2) * W.preΨ' 3 *
        if Even 3 then W.Ψ₂Sq else 1) =
    X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)
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
⊢ (W.map f).ψ₂ = Polynomial.map (mapRingHom f) W.ψ₂

Tactic:
by
  simp_rw [ψ₂, Affine.map_polynomialY]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ W.c₆ = 0

Tactic:
rw [c₆_of_isShortNF]
  linear_combination -288 * W.a₆ * CharP.cast_eq_zero R 3

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

Goal state before:
pp: case a₄
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this✝ : Invertible 2 := ⋯
W' : WeierstrassCurve F := ⋯
this : W'.IsCharNeTwoNF
⊢ ({ u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 } • W').a₄ = 0

Tactic:
have ha₂ : W'.a₂ ≠ 0 := W.toShortNFOfCharThree_a₂ ▸ hb₂
    simp [field, variableChange_a₄, -mul_eq_zero]
    linear_combination (W'.a₄ * W'.a₂ ^ 2 + W'.a₄ ^ 2) * CharP.cast_eq_zero F 3

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
⊢ W.b₂ = 1 + 4 * W.a₂

Tactic:
rw [b₂, a₁_of_isCharTwoJNeZeroNF]
  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]; simp

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
n : Fin 3
⊢ (⇑f ∘ (u • P)) n = (f u • ⇑f ∘ P) n

Tactic:
fin_cases n <;> simp only [smul_fin3, comp_fin3]

Goal state after:
case «0»
R : Type r
inst✝¹ : CommRing R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ ![f (u ^ 2 * P x), f (u ^ 3 * P y), f (u * P z)] ⟨0, ⋯⟩ =
    ![f u ^ 2 * (⇑f ∘ P) x, f u ^ 3 * (⇑f ∘ P) y, f u * (⇑f ∘ P) z] ⟨0, ⋯⟩

case «1»
R : Type r
inst✝¹ : CommRing R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ ![f (u ^ 2 * P x), f (u ^ 3 * P y), f (u * P z)] ⟨1, ⋯⟩ =
    ![f u ^ 2 * (⇑f ∘ P) x, f u ^ 3 * (⇑f ∘ P) y, f u * (⇑f ∘ P) z] ⟨1, ⋯⟩

case «2»
R : Type r
inst✝¹ : CommRing R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ ![f (u ^ 2 * P x), f (u ^ 3 * P y), f (u * P z)] ⟨2, ⋯⟩ =
    ![f u ^ 2 * (⇑f ∘ P) x, f u ^ 3 * (⇑f ∘ P) y, f u * (⇑f ∘ P) z] ⟨2, ⋯⟩
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
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
⊢ 2 ≠ 0

Tactic:
rw [show (2 : F) = -1 by linear_combination CharP.cast_eq_zero F 3, neg_ne_zero]
    exact one_ne_zero

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ W'.Equation 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:
Equation,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P) W'.polynomial = 0 ↔
    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.IsomOfJ

Goal state before:
pp: case inr
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
heq : E.j = E'.j
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
this : ∀ (E : WeierstrassCurve F) [inst : E.IsElliptic], E.j = E'.j → E.IsShortNF → ∃ C, C • E = E'
h✝ : ¬E.IsShortNF
C : VariableChange F
hE : (C • E).IsShortNF
⊢ ∃ C, C • E = E'

Tactic:
rw [← variableChange_j E C] at heq

Goal state after:
case inr
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
this : ∀ (E : WeierstrassCurve F) [inst : E.IsElliptic], E.j = E'.j → E.IsShortNF → ∃ C, C • E = E'
h✝ : ¬E.IsShortNF
C : VariableChange F
heq : (C • E).j = E'.j
hE : (C • E).IsShortNF
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
⊢ (W'.map f).Equation (⇑f ∘ P)

Tactic:
Equation,

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
⊢ (eval (⇑f ∘ P)) (W'.map f).polynomial = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ W.toAffine.addX (P x / P z ^ 2) (P x / P z ^ 2) (-n / (P z * d)) =
    (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2) / (P z * d) ^ 2

Tactic:
by
  simp [field]
  ring1

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

Goal state before:
pp: A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x✝ : TopologicalSpace A := hB.topology
a : A
a_in : a ∈ (B i).carrier
⊢ ∃ i_1, True ∧ {b | b - a ∈ B i_1} ⊆ (B i).carrier

Tactic:
use i, trivial

Goal state after:
case right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x✝ : TopologicalSpace A := ⋯
a : A
a_in : a ∈ (B i).carrier
⊢ {b | b - a ∈ B i} ⊆ (B i).carrier
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 : ↥(posSubmonoid R)
⊢ ∀ (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:
s

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 : ↥(posSubmonoid R)
⊢ ∀ (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)
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 : ↥(posSubmonoid R)
⊢ ∀ (s : ↥(posSubmonoid R)),
    x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → ValueGroupWithZero.mk (x ^ n) (s ^ n) = ValueGroupWithZero.mk (y ^ n) (t ^ n)

Tactic:
s

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)
⊢ 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 : ↥(posSubmonoid R)
⊢ ∀ (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:
s

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 : ↥(posSubmonoid R)
⊢ ∀ (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)
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
⊢ s ∈ 𝓝 0 ↔ ∃ γ, {x | v.restrict x < ↑γ} ⊆ s

Tactic:
Filter.hasBasis_iff.mp v.subgroups_basis.hasBasis_nhds_zero s

Goal state after:
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
⊢ (∃ i, True ∧ ↑(v.ltAddSubgroup ((Units.map ↑embedding) i)) ⊆ s) ↔ ∃ γ, {x | v.restrict x < ↑γ} ⊆ s
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
h : ∃ y, v.restrict y < ↑1 ∧ y ≠ 0
⊢ ∃ x, x ≠ 0 ∧ v x ≠ 1

Tactic:
obtain ⟨x, hx, hx'⟩ := h

Goal state after:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
hx : v.restrict x < ↑1
hx' : x ≠ 0
⊢ ∃ x, x ≠ 0 ∧ v x ≠ 1
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 : ↥(posSubmonoid R)
⊢ ∀ (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:
s

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)
⊢ 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: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ y✝ : R
h : x✝ * y✝ ∈ supp R
⊢ x✝ ∈ supp R ∨ y✝ ∈ supp R

Tactic:
by_contra! h'

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ y✝ : R
h : x✝ * y✝ ∈ supp R
h' : x✝ ∉ supp R ∧ y✝ ∉ supp R
⊢ False
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case h
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
h : ∃ y, v.restrict y < ↑1 ∧ y ≠ 0
⊢ ∃ x, x ≠ 0 ∧ v x ≠ 1

Tactic:
obtain ⟨x, hx, hx'⟩ := h

Goal state after:
case h
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
x : R
hx : v.restrict x < ↑1
hx' : x ≠ 0
⊢ ∃ x, x ≠ 0 ∧ v x ≠ 1
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

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

Tactic:
rw [inv_le_comm₀ uniformizer_pos ha, le_uniformizer_iff, inv_lt_one₀ ha]

Goal state after:
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
x y : R
r : ↥(posSubmonoid R)
⊢ ∀ (s : ↥(posSubmonoid R)),
    x * ↑r ≤ᵥ y * ↑s →
      y * ↑s ≤ᵥ x * ↑r →
        (restrict₀ (ofClass v)) x / (restrict₀ (ofClass v)) ↑s = (restrict₀ (ofClass v)) y / (restrict₀ (ofClass v)) ↑r

Tactic:
s

Goal state after:
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
x y : R
r s : ↥(posSubmonoid R)
⊢ x * ↑r ≤ᵥ y * ↑s →
    y * ↑s ≤ᵥ x * ↑r →
      (restrict₀ (ofClass v)) x / (restrict₀ (ofClass v)) ↑s = (restrict₀ (ofClass v)) y / (restrict₀ (ofClass v)) ↑r
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 Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
r : (ofClass v).ValueGroup₀
⊢ IsClosed[_t] {x | v.restrict x < r}

Tactic:
by
  rcases eq_or_ne r 0 with rfl | hr
  · simp
  exact AddSubgroup.isClosed_of_isOpen (Valuation.ltAddSubgroup v.restrict (Units.mk0 r hr))
    (isOpen_ball _)

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

Goal state before:
pp: A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hπ : exp (-1) ∈ range ⇑v
this : Units.mk0 (exp (-1)) ⋯ = Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup
⊢ Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup =
    Units.mk0 (exp (-1)) generator_eq_exp_neg_one_of_mem_range._proof_1

Tactic:
by
    simp [← this]

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

Goal state before:
pp: case h
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 = ↑γ
x : WithVal v
hx :
  x ∈
    {x |
      Valued.v.restrict x <
        ↑(Units.mk0 (Valued.v.restrict ((equiv v).symm r) / Valued.v.restrict ((equiv v).symm s)) ⋯)}
y : R := (equiv v) x
hy : toVal v y = x
⊢ (equiv v) x ∈ {x | Valued.v.restrict x < ↑γ}

Tactic:
have hs0' : 0 < Valued.v.restrict (toVal v s) := by
    simp [restrict_pos_iff, h.pos_iff, ← hv, hs₀]

Goal state after:
case h
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 = ↑γ
x : WithVal v
hx :
  x ∈
    {x |
      Valued.v.restrict x <
        ↑(Units.mk0 (Valued.v.restrict ((equiv v).symm r) / Valued.v.restrict ((equiv v).symm s)) ⋯)}
y : R := (equiv v) x
hy : toVal v y = x
hs0' : 0 < Valued.v.restrict (toVal v s)
⊢ (equiv v) x ∈ {x | Valued.v.restrict x < ↑γ}
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: case refine_3
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
x : X
hx : ↑x ∈ s
y : X
hy : ↑y ∈ s
hxy : x < y
this : ⟨↑x, hx⟩ < ⟨↑y, hy⟩
z : { x // x ∈ s }
hz : ↑x < ↑z
hz' : ↑z < ↑y
⊢ (↑z).unbot ⋯ < y

Tactic:
rw [← WithBot.coe_lt_coe]
    simp [hz'.trans_le']

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
h : b = |a|ₘ ∧ 1 < b
this : ∀ {a : G}, b = |a|ₘ ∧ 1 < b → 1 ≤ a → IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
ha : ¬1 ≤ a
⊢ 1 ≤ a⁻¹

Tactic:
by simpa using le_of_not_ge ha

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b ↔ b = |a|ₘ ∧ 1 < b

Tactic:
by
  constructor <;> intro h
  · have := Subgroup.cyclic_of_min h
    have ha : a ∈ closure ({b} : Set G) := by
      simp [← this]
    rw [mem_closure_singleton] at ha
    obtain ⟨n, rfl⟩ := ha
    have := h.left
    simp only [mem_closure_singleton, mem_ofPred_eq] at this
    obtain ⟨m, hm⟩ := this.left
    have key : m * n = 1 := by
      rw [← zpow_right_inj this.right, zpow_mul', hm, zpow_one]
    rw [Int.mul_eq_one_iff_eq_one_or_neg_one] at key
    rw [eq_comm]
    rcases key with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ <;>
    simp [this.right.le, this.right, mabs]
  · wlog ha : 1 ≤ a generalizing a
    · convert! @this (a⁻¹) ?_ (by simpa using le_of_not_ge ha) using 4
      · simp
      · rwa [mabs_inv]
    rw [mabs, sup_eq_left.mpr ((inv_le_one'.mpr ha).trans ha)] at h
    rcases h with ⟨rfl, h⟩
    refine ⟨?_, ?_⟩
    · simp [h]
    · intro x
      simp only [mem_closure_singleton, mem_ofPred_eq, and_imp, forall_exists_index]
      rintro k rfl hk
      rw [← zpow_one b, ← zpow_mul, one_mul, zpow_le_zpow_iff_right h, ← zero_add 1,
          ← Int.lt_iff_add_one_le]
      contrapose! hk
      rw [← Left.one_le_inv_iff, ← zpow_neg]
      exact one_le_zpow ha (by simp [hk])

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) φ = (coeff n) ψ
n : Unit →₀ ℕ
⊢ (coeff ?m.21) φ = (coeff ?m.21) ψ

pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) φ = (coeff n) ψ
n : Unit →₀ ℕ
⊢ n () = ?m.21

pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) φ = (coeff n) ψ
n : Unit →₀ ℕ
⊢ ℕ

Tactic:
· apply h

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) φ = (coeff n) ψ
n : Unit →₀ ℕ
⊢ n () = ?m.21

R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) φ = (coeff n) ψ
n : Unit →₀ ℕ
⊢ ℕ
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ ∑ p_1 ∈ antidiagonal (d + n), (coeff p_1.1) (X ^ n) * (coeff p_1.2) p = (coeff d) p

Tactic:
Finset.sum_eq_single (n, d),

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (coeff (n, d).1) (X ^ n) * (coeff (n, d).2) p = (coeff d) p

case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (n, d) → (coeff b.1) (X ^ n) * (coeff b.2) p = 0

case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (n, d) ∉ antidiagonal (d + n) → (coeff (n, d).1) (X ^ n) * (coeff (n, d).2) p = 0
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
hxy : v xy = embedding a * embedding b
hx : v x = embedding a
hy : v y = embedding b
hx0 : ¬x = 0
hy0 : y = 0
⊢ (if h : extensionValuation ↑xy = 0 then 0 else ↑⟨Units.mk0 (v xy) ⋯, ⋯⟩) =
    if h : extensionValuation ↑y = 0 then 0
    else if h : extensionValuation ↑x = 0 then 0 else ↑⟨Units.mk0 (v x) ⋯, ⋯⟩ * ↑⟨Units.mk0 (v y) ⋯, ⋯⟩

Tactic:
simpa [← hy, hy0] using hxy

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

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
hxy : v xy = embedding a * embedding b
hx : v x = embedding a
hy : v y = embedding b
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ↑⟨Units.mk0 (v xy) ⋯, ⋯⟩ = ↑⟨Units.mk0 (v x) ⋯, ⋯⟩ * ↑⟨Units.mk0 (v y) ⋯, ⋯⟩

Tactic:
simp only [← WithZero.coe_mul, MulMemClass.mk_mul_mk, WithZero.coe_inj, Subtype.mk.injEq]

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
hxy : v xy = embedding a * embedding b
hx : v x = embedding a
hy : v y = embedding b
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ Units.mk0 (v xy) ⋯ = Units.mk0 (v x) ⋯ * Units.mk0 (v y) ⋯