mathlib-initiative/mathlib-tactics huggingface dataset:
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

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

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

Goal state after:
case mpr
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
⊢ (∃ i, True ∧ ↑(B i) ⊆ s) → ∃ i ∈ hB.toRingFilterBasis.toAddGroupFilterBasis, id i ⊆ s
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
a : A
s : Set A
i : ι
hi : (fun y ↦ a + y) '' ↑(B i) ⊆ s
h : {b | b - a ∈ B i} = (fun y ↦ a + y) '' ↑(B i)
⊢ {b | b - a ∈ B i} ⊆ s

Tactic:
h

Goal state after:
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y ↦ a + y) '' ↑(B i) ⊆ s
h : {b | b - a ∈ B i} = (fun y ↦ a + y) '' ↑(B i)
⊢ (fun y ↦ a + y) '' ↑(B i) ⊆ s
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
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ ¬P x / P z ^ 2 = Q x / Q z ^ 2

Tactic:
← X_eq_iff hPz hQz

Goal state after:
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ ¬P x * Q z ^ 2 = Q x * P z ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ toAffine W (W.neg P) = -toAffine W P

Tactic:
rw [neg_of_Z_eq_zero hP hPz,
      toAffine_smul _ ((isUnit_Y_of_Z_eq_zero hP hPz).div <| isUnit_X_of_Z_eq_zero hP hPz).neg,
      toAffine_zero, toAffine_of_Z_eq_zero hPz, Affine.Point.neg_zero]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (i j : (ofClass v).ValueGroup₀ˣ),
    ∃ k,
      v.ltAddSubgroup ((Units.map ↑embedding) k) ≤
        v.ltAddSubgroup ((Units.map ↑embedding) i) ⊓ v.ltAddSubgroup ((Units.map ↑embedding) j)

Tactic:
rintro γ₀ γ₁
      use min γ₀ γ₁
      have hmin : embedding (min γ₀.1 γ₁.1) = min (embedding γ₀.1) (embedding γ₁.1) :=
        embedding_strictMono.monotone.map_inf γ₀.1 γ₁.1
      simp [ltAddSubgroup, hmin]
      tauto

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
⊢ ∀ (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:
z

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

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z : R
⊢ ∀ (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)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ supp R ≠ ⊤

Tactic:
rw [Ideal.ne_top_iff_one]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ 1 ∉ supp 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
⊢ IsOpen[_i.toTopologicalSpace] {x | v.restrict x ≤ r}

Tactic:
rw [isOpen_iff_mem_nhds]
  intro x hx
  rw [mem_nhds]
  simp only [ofPred_subset_ofPred]
  exact ⟨Units.mk0 _ hr, fun y hy ↦
    (sub_add_cancel y x).symm ▸ le_trans (v.restrict.map_add _ _) (max_le (le_of_lt hy) hx)⟩

Goal state after:
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
h : {x | v.restrict x = r} = {x | v.restrict x ≤ r} \ {x | v.restrict x < r}
⊢ IsClopen {x | v.restrict x = r}

Tactic:
h

Goal state after:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
h : {x | v.restrict x = r} = {x | v.restrict x ≤ r} \ {x | v.restrict x < r}
⊢ IsClopen ({x | v.restrict x ≤ r} \ {x | v.restrict x < 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
  rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]
  intro x hx
  simp only [mem_compl_iff, mem_ofPred_eq, not_le] at hx
  rw [v.mem_nhds_iff]
  have hx' : v.restrict x ≠ 0 := hx.ne_zero
  exact ⟨Units.mk0 _ hx', fun y hy hy' ↦ ne_of_lt hy <| map_sub_swap v.restrict x y ▸
      (Valuation.map_sub_eq_of_lt_left _ <| lt_of_le_of_lt hy' hx)⟩

Goal state after:
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₀
hr : r ≠ 0
h : {x | v.restrict x = r} = {x | v.restrict x ≤ r} \ {x | v.restrict x < r}
⊢ IsClopen {x | v.restrict x = r}

Tactic:
h

Goal state after:
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
h : {x | v.restrict x = r} = {x | v.restrict x ≤ r} \ {x | v.restrict x < r}
⊢ IsClopen ({x | v.restrict x ≤ r} \ {x | v.restrict x < r})
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✝¹ x✝ : ValueGroupWithZero R
x y : R
⊢ ∀ (a : R) (b : 0 <ᵥ a) (a_1 : R) (b_1 : 0 <ᵥ a_1),
    ((if h : (ofClass v) y = 0 then 0
        else
          if h : (ofClass v) x = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩) /
        if h : (ofClass v) a_1 = 0 then 0
        else
          if h : (ofClass v) a = 0 then 0
          else ↑⟨Units.mk0 ((ofClass v) a) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) a_1) ⋯, ⋯⟩) =
      ((if h : (ofClass v) x = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) x) h, ⋯⟩) /
          if h : (ofClass v) a = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) a) ⋯, ⋯⟩) *
        ((if h : (ofClass v) y = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) y) h, ⋯⟩) /
          if h : (ofClass v) a_1 = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) a_1) ⋯, ⋯⟩)

Tactic:
z

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✝¹ x✝ : ValueGroupWithZero R
x y z : R
⊢ ∀ (b : 0 <ᵥ z) (a : R) (b_1 : 0 <ᵥ a),
    ((if h : (ofClass v) y = 0 then 0
        else
          if h : (ofClass v) x = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩) /
        if h : (ofClass v) a = 0 then 0
        else
          if h : (ofClass v) z = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) a) ⋯, ⋯⟩) =
      ((if h : (ofClass v) x = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) x) h, ⋯⟩) /
          if h : (ofClass v) z = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩) *
        ((if h : (ofClass v) y = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) y) h, ⋯⟩) /
          if h : (ofClass v) a = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) a) ⋯, ⋯⟩)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
γ : ValueGroupWithZero R
⊢ embedding ((embed (valuation R)) γ) = γ

Tactic:
by
  induction γ using ValueGroupWithZero.ind
  simp [mk_eq_div]

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

Goal state before:
pp: R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a b : ValueGroupWithZero R
⊢ a < b → (embed v) a < (embed v) b

Tactic:
h

Goal state after:
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a b : ValueGroupWithZero R
h : a < b
⊢ (embed v) a < (embed v) b
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
hm₀ : 0 ≤ m
n : ℕ
hn : m = ↑n
hpow : v (↑π.val ^ (-m) * ↑r) = 1
a : ↥v.valuationSubring := ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha : a = ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
⊢ ¬(↑π.val = 0 ∧ n ≠ 0)

Tactic:
not_and_or

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
hm₀ : 0 ≤ m
n : ℕ
hn : m = ↑n
hpow : v (↑π.val ^ (-m) * ↑r) = 1
a : ↥v.valuationSubring := ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha : a = ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
⊢ ¬↑π.val = 0 ∨ ¬n ≠ 0
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
⊢ ∀ (ib : (ofClass Valued.v).ValueGroup₀ˣ),
    ∃ ia, ∀ x ∈ {x | Valued.v.restrict x < ↑ia}, (equiv v) x ∈ {x | Valued.v.restrict x < ↑ib}

Tactic:
intro γ

Goal state after:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
γ : (ofClass Valued.v).ValueGroup₀ˣ
⊢ ∃ ia, ∀ x ∈ {x | Valued.v.restrict x < ↑ia}, (equiv v) x ∈ {x | Valued.v.restrict 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 Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
⊢ ∀ (ib : (ofClass Valued.v).ValueGroup₀ˣ),
    ∃ ia, ∀ x ∈ {x | Valued.v.restrict x < ↑ia}, (equiv v).symm x ∈ {x | Valued.v.restrict x < ↑ib}

Tactic:
intro γ

Goal state after:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
⊢ ∃ ia, ∀ x ∈ {x | Valued.v.restrict x < ↑ia}, (equiv v).symm x ∈ {x | Valued.v.restrict 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)) *
        ((valuation K (maximalIdeal A)) ((algebraMap A K) (π ^ m)))⁻¹ *
      1⁻¹ ≤
    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:
inv_one,

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)) *
        ((valuation K (maximalIdeal A)) ((algebraMap A K) (π ^ m)))⁻¹ *
      1 ≤
    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: case ih
Γ₀ : 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
a : WithVal v
⊢ Valued.v ↑a ≤ 1 ↔ Valued.v ((mapEquiv h.uniformEquiv) ↑a) ≤ 1

Tactic:
simpa [Valued.valuedCompletion_apply] using! h.le_one_iff_le_one

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

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ ∀ (γ₀ : (ofClass v).ValueGroup₀), γ₀ ≠ 0 → ∀ᶠ (x : K) in 𝓝 0, v.restrict x < γ₀

Tactic:
intro γ

Goal state after:
case inl
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : (ofClass v).ValueGroup₀
⊢ γ ≠ 0 → ∀ᶠ (x : K) in 𝓝 0, v.restrict x < γ
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective ⇑v
⊢ ∀ (γ₀ : Γ₀), γ₀ ≠ 0 → ∀ᶠ (x : K) in 𝓝 0, v x < γ₀

Tactic:
intro γ

Goal state after:
case inl
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective ⇑v
γ : Γ₀
⊢ γ ≠ 0 → ∀ᶠ (x : K) in 𝓝 0, v x < γ
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 Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ : ∀ x ∈ M₀, ↑γ₀ ≤ v.restrict x
hF : ∀ (γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ
⊢ ∀ (γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ),
    ∃ M ∈ map (fun x ↦ x⁻¹) F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ

Tactic:
intro γ

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ : ∀ x ∈ M₀, ↑γ₀ ≤ v.restrict x
hF : ∀ (γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
⊢ ∃ M ∈ map (fun x ↦ x⁻¹) F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ
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 Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₁ : x ∈ M₁
y : K
H₁ : v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
left✝ : y ∈ M₀
y_in₁ : y ∈ M₁
x_in₀ : ↑γ₀ ≤ v.restrict x
h : v.restrict x = 0
⊢ False

Tactic:
h

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₁ : x ∈ M₁
y : K
H₁ : v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
left✝ : y ∈ M₀
y_in₁ : y ∈ M₁
x_in₀ : ↑γ₀ ≤ 0
h : v.restrict x = 0
⊢ False
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y | y ∈ closure {b ^ n} ∧ 1 < y} b
this✝ : closure {b ^ n} = closure {b}
this : (∃ n_1, (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
⊢ b ^ (m * n) = b ^ 1

Tactic:
zpow_mul',

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y | y ∈ closure {b ^ n} ∧ 1 < y} b
this✝ : closure {b ^ n} = closure {b}
this : (∃ n_1, (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
⊢ (b ^ n) ^ m = b ^ 1
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : v.restrict z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑a = (fun x ↦ x * x₀) y
⊢ (ValueGroup₀.restrict₀ (ofClass v)) (a * z₀⁻¹) = 1

Tactic:
ValueGroup₀.restrict₀_eq_one_iff

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : v.restrict z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑a = (fun x ↦ x * x₀) y
⊢ (ofClass v) (a * z₀⁻¹) = 1
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : hat K
h✝ : x ≠ 0
hr : ∀ (r : K), embedding ((restrict₀ (ofClass v)) r) = v r
h : ∀ (a b : (ofClass v).ValueGroup₀), embedding a = embedding b ↔ a = b
⊢ IsClosed {b | ∃ r, embedding (extension b) = embedding (v.restrict r)}

Tactic:
h

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : hat K
h✝ : x ≠ 0
hr : ∀ (r : K), embedding ((restrict₀ (ofClass v)) r) = v r
h : ∀ (a b : (ofClass v).ValueGroup₀), embedding a = embedding b ↔ a = b
⊢ IsClosed {b | ∃ r, extension b = v.restrict r}
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_5
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
a✝² : G₀
a✝¹ : g ≤ a✝²
ha0 : ¬a✝² = 0
b✝ : G₀
a✝ : g ≤ b✝
hb0 : ¬b✝ = 0
⊢ a✝² < b✝ → (if h : a✝² = 0 then 1 else Units.mk0 a✝² h) < if h : b✝ = 0 then 1 else Units.mk0 b✝ h

Tactic:
h

Goal state after:
case refine_5
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h✝ : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
a✝² : G₀
a✝¹ : g ≤ a✝²
ha0 : ¬a✝² = 0
b✝ : G₀
a✝ : g ≤ b✝
hb0 : ¬b✝ = 0
h : a✝² < b✝
⊢ (if h : a✝² = 0 then 1 else Units.mk0 a✝² h) < if h : b✝ = 0 then 1 else Units.mk0 b✝ h
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case neg
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
⊢ ∃ C, IsIntegral R (C • W)

Tactic:
· have hlmax_ge_1 : lmax ≥ 1 := le_of_not_ge hlmax_le_1
    have h : ∃ a : K, valuation R K a = lmax := by
      let i : ℕ := l.idxOf lmax
      have hi : i < l.length := List.idxOf_lt_length_of_mem hlmax_mem
      use l₀[i]
      have hi₁ : (valuation R K) l₀[i] = l[i] := by simp [l]
      simpa only [hi₁] using (List.getElem_idxOf hi)
    choose a ha using h
    have ha₀ : a ≠ 0 := by
      by_contra ha₀; simp only [ha₀, map_zero] at ha
      exact (ha ▸ hlmax_le_1) zero_le_one
    use ⟨Units.mk0 a ha₀, 0, 0, 0⟩
    apply isIntegral_of_exists_lift R
    all_goals
      apply (mem_integer_iff _ _ _).mp
      simp only [variableChange_def, Units.val_inv_eq_inv_val, Units.val_mk0, mul_zero, add_zero,
        inv_pow, zero_mul, sub_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]
      apply (Valuation.mem_integer_iff _ _).mpr
      simp only [map_mul, map_inv₀, map_pow, ha]
      refine inv_mul_le_one_of_le₀ ?_ zero_le
      refine (hlmax _ (by simp [l₀, l])).trans ?_
    any_goals
      apply le_self_pow hlmax_ge_1.le
      linarith
    rfl

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

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

Tactic:
simp only [mem_ofPred_eq, Function.onFun, gt_iff_lt]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
⊢ (coeff d) (p * X ^ n) = 0

Tactic:
refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ (coeff x.1) p * (coeff x.2) (X ^ n) = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
⊢ (coeff d) (X ^ n * p) = 0

Tactic:
refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ (coeff x.1) (X ^ n) * (coeff x.2) p = 0