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

Goal state before:
pp: I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofiltered I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
J : Type u_1
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
⊢ ∃ i s V, IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U ↑j = c.π.app i ⁻¹ᵁ V j

Tactic:
by
  have := compactSpace_of_isLimit D c hc
  obtain ⟨s, hs⟩ := isCompact_univ.elim_finite_subcover _
    (fun i ↦ (U i).isOpen) hU.iSup_set_eq_univ.ge
  have hU : IsOpenCover fun j : s ↦ U ↑j := by
    simpa only [IsOpenCover, eq_top_iff, ← SetLike.coe_subset_coe, Opens.coe_top, Opens.iSup_mk,
      Opens.carrier_eq_coe, Opens.coe_mk, Set.iUnion_subtype]
  obtain ⟨i, V, hV, heq⟩ := Scheme.exists_isOpenCover_and_isAffine_of_finite _ _ hc _ hU (hU' ·)
  use i, s, V, hV

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ W.ΨSq (2 * m) =
    (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) ^ 2 * W.Ψ₂Sq

Tactic:
rw [ΨSq, preΨ_even, if_pos <| even_two_mul m]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (mk W) (C (W.preΨ n)) ^ 2 * (if Even n then (mk W) W.ψ₂ else (mk W) 1) ^ 2 =
    (mk W) (C (W.preΨ n ^ 2)) * if Even n then (mk W) (C W.Ψ₂Sq) else (mk W) (C 1)

Tactic:
ite_pow,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ ((mk W) (C (W.preΨ n)) ^ 2 * if Even n then (mk W) W.ψ₂ ^ 2 else (mk W) 1 ^ 2) =
    (mk W) (C (W.preΨ n ^ 2)) * if Even n then (mk W) (C W.Ψ₂Sq) else (mk W) (C 1)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 4 ≠ 0
⊢ W.Ψ₂Sq.coeff 3 ≠ 0

Tactic:
by
  rwa [coeff_Ψ₂Sq]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (mk W) (C X) * (mk W) (C (W.ΨSq n)) -
      (mk W) (C (W.preΨ (n + 1))) * (mk W) (C (W.preΨ (n - 1))) * (if Even n then (mk W) 1 else (mk W) W.ψ₂) ^ 2 =
    (mk W) (C X) * (mk W) (C (W.ΨSq n)) -
      (mk W) (C (W.preΨ (n + 1))) * (mk W) (C (W.preΨ (n - 1))) * if Even n then (mk W) (C 1) else (mk W) (C W.Ψ₂Sq)

Tactic:
ite_pow,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ ((mk W) (C X) * (mk W) (C (W.ΨSq n)) -
      (mk W) (C (W.preΨ (n + 1))) * (mk W) (C (W.preΨ (n - 1))) * if Even n then (mk W) 1 ^ 2 else (mk W) W.ψ₂ ^ 2) =
    (mk W) (C X) * (mk W) (C (W.ΨSq n)) -
      (mk W) (C (W.preΨ (n + 1))) * (mk W) (C (W.preΨ (n - 1))) * if Even n then (mk W) (C 1) else (mk W) (C W.Ψ₂Sq)
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:
← map_Φ,

Goal state after:
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 = ((W⁄A).map ↑f).Φ n
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ 4 * W.a₂ = W.a₂

Tactic:
linear_combination W.a₂ * CharP.cast_eq_zero R 3

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.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
h : W.Δ ≠ 0
⊢ W.j = -W.a₂ ^ 3 / W.a₆

Tactic:
Δ_of_isCharThreeJNeZeroNF_of_char_three

Goal state after:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
h : -W.a₂ ^ 3 * W.a₆ ≠ 0
⊢ W.j = -W.a₂ ^ 3 / W.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case h.a₃
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ ({ u := 1, r := 0, s := s, t := 0 } • E).a₃ = E'.a₃

Tactic:
simp_rw [variableChange_a₃, inv_one, Units.val_one, a₃_of_isCharTwoJNeZeroNF]
    ring1

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
⊢ (eval P) W'.polynomial =
    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)

Tactic:
by
  rw [polynomial]
  simp

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

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

Tactic:
convert! (W.natDegree_coeff_preΨ' n).right using 1

Goal state after:
case e'_3
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ ↑(if Even n then n / 2 else n) = ↑(expCoeff n)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

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

Tactic:
induction n using Int.negInduction with

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

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

Tactic:
exact_mod_cast W.preΨ_ofNat n ▸ W.coeff_preΨ' n

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

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

Tactic:
induction n using Int.negInduction with

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

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

Tactic:
induction n using Int.negInduction with

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
hn : 2 < n.natAbs
h : ↑n ≠ 0
⊢ 0 < (W.preΨ n).natDegree

Tactic:
induction n using Int.negInduction with

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℤ
h : ↑n ≠ 0
⊢ W.preΨ n ≠ 0

Tactic:
induction n using Int.negInduction with

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (W.ΨSq n).natDegree ≤ n.natAbs ^ 2 - 1

Tactic:
induction n using Int.negInduction with

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (W.ΨSq n).coeff (n.natAbs ^ 2 - 1) = ↑n ^ 2

Tactic:
induction n using Int.negInduction with

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W'.a₁ * P x * P y ≠ 0)
hPz : P z = 0
hPx : P x ≠ 0
hPy : P y = 0
⊢ False

Tactic:
equation_of_Z_eq_zero hPz,

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : P y ^ 2 = P x ^ 3 ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W'.a₁ * P x * P y ≠ 0)
hPz : P z = 0
hPx : P x ≠ 0
hPy : P y = 0
⊢ False
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.dblZ (u • P) = u ^ 4 * W'.dblZ P

Tactic:
simp only [dblZ, negY_smul, smul_fin3_ext]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ u * P z * (u ^ 3 * P y - u ^ 3 * W'.negY P) = u ^ 4 * (P z * (P y - W'.negY P))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (W.Φ ↑n).natDegree ≤ n ^ 2 ∧ (W.Φ ↑n).coeff (n ^ 2) = 1

Tactic:
by
  let dm {m n p q} : _ → _ → (p * q : R[X]).natDegree ≤ m + n := natDegree_mul_le_of_le
  let dp {m n p} : _ → (p ^ n : R[X]).natDegree ≤ n * m := natDegree_pow_le_of_le n
  let cm {m n p q} : _ → _ → (p * q : R[X]).coeff (m + n) = _ := coeff_mul_add_eq_of_natDegree_le
  let h {n} := W.natDegree_coeff_preΨ' n
  rcases n with _ | _ | n
  iterate 2 simp [natDegree_X_le]
  have hd : (n + 1 + 1) ^ 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3 := by
    push_cast [← @Nat.cast_inj ℤ, expDegree_cast (n + 1).succ_ne_zero, Nat.even_add_one, ite_not]
    split_ifs <;> ring1
  have hd' : (n + 1 + 1) ^ 2 =
      expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0 := by
    push_cast [← @Nat.cast_inj ℤ, ← mul_left_cancel_iff_of_pos (b := (_ ^ 2 : ℤ)) two_pos, mul_add,
      expDegree_cast (n + 2).succ_ne_zero, expDegree_cast n.succ_ne_zero, Nat.even_add_one, ite_not]
    split_ifs <;> ring1
  have hc : (1 : ℤ) = 1 * expCoeff (n + 2) ^ 2 * (if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * (if Even (n + 1) then 4 else 1) := by
    push_cast [← @Int.cast_inj ℚ, expCoeff_cast, Nat.even_add_one, ite_not]
    split_ifs <;> ring1
  rw [Nat.cast_add, Nat.cast_one, Φ_ofNat]
  constructor
  · nth_rw 1 [← max_self <| (_ + _) ^ 2, hd, hd']
    refine natDegree_sub_le_of_le (dm (dm natDegree_X_le (dp h.1)) ?_) (dm (dm h.1 h.1) ?_) <;>
      split_ifs <;> simp only [natDegree_one.le, W.natDegree_Ψ₂Sq_le]
  · nth_rw 1 [coeff_sub, hd, hd', cm (dm natDegree_X_le (dp h.1)), cm natDegree_X_le (dp h.1),
      coeff_X_one, coeff_pow_of_natDegree_le h.1, h.2, apply_ite₂ coeff, coeff_one_zero, coeff_Ψ₂Sq,
      cm (dm h.1 h.1), cm h.1 h.1, h.2, h.2, apply_ite₂ coeff, coeff_one_zero, coeff_Ψ₂Sq]
    conv_rhs => rw [← Int.cast_one, hc]
    · norm_cast
    all_goals split_ifs <;> simp only [natDegree_one.le, W.natDegree_Ψ₂Sq_le]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (W.Φ n).natDegree ≤ n.natAbs ^ 2

Tactic:
induction n using Int.negInduction with

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (W.Φ n).coeff (n.natAbs ^ 2) = 1

Tactic:
induction n using Int.negInduction with

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
⊢ W.dblXYZ P = P x ^ 2 • ![1, 1, 0]

Tactic:
dblXYZ_of_Z_eq_zero hP.left hPz

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
⊢ P x ^ 2 • ![1, 1, 0] = P x ^ 2 • ![1, 1, 0]
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ addZ P Q = 0

Tactic:
by
  rw [addZ, hx, sub_self]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
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:
intro x y t s h₁ 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
h₂ : y * ↑s ≤ᵥ x * ↑t
⊢ ValueGroupWithZero.mk (x ^ n) (s ^ n) = ValueGroupWithZero.mk (y ^ n) (t ^ n)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
S : Type s
F : Type u
K : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field F
inst✝⁷ : Field K
W' : Jacobian R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R F
inst✝⁴ : Algebra S F
inst✝³ : IsScalarTower R S F
inst✝² : Algebra R K
inst✝¹ : Algebra S K
inst✝ : IsScalarTower R S K
f : F →ₐ[S] K
P Q : Fin 3 → F
hP : (W'⁄F).Nonsingular P
hQ : (W'⁄F).Nonsingular Q
⊢ (W'⁄K).add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ (W'⁄F).add P Q

Tactic:
rw [← RingHom.coe_coe, ← WeierstrassCurve.Jacobian.map_add _ hP hQ, map_baseChange]

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

Goal state before:
pp: case e'_5
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x✝ : (ofClass v).ValueGroup₀ˣ
⊢ {p | v.restrict (p.2 - p.1) < ↑x✝} = (fun p ↦ p.2 + -p.1) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) x✝))

Tactic:
restrict_lt_iff_lt_embedding,

Goal state after:
case e'_5
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x✝ : (ofClass v).ValueGroup₀ˣ
⊢ {p | v (p.2 - p.1) < embedding ↑x✝} = (fun p ↦ p.2 + -p.1) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) x✝))
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 Γ₀
x : R
hx : v.restrict x < ↑1
hx' : x ≠ 0
⊢ ∃ x, x ≠ 0 ∧ v x ≠ 1

Tactic:
restrict_lt_iff_lt_embedding,

Goal state after:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
hx : v x < embedding ↑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 : R
⊢ ∀ (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:
intro x y t s h₁ 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
h₂ : 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 mp
R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
r : ValueGroupWithZero R
hr : r ≠ 0
hr' : r ≠ 1
⊢ v.IsNontrivial

Tactic:
induction r using ValueGroupWithZero.ind with

Goal state after:
case mp.mk
R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
⊢ v.IsNontrivial
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: 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

Tactic:
simp [valuation, div_eq_mul_inv, ValueGroupWithZero.inv_mk (b : R) 1 b.prop]

Goal state after:
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
x : R
hx : v.restrict x < ↑1
hx' : x ≠ 0
⊢ ∃ x, x ≠ 0 ∧ v x ≠ 1

Tactic:
restrict_lt_iff_lt_embedding,

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 x < embedding ↑1
hx' : x ≠ 0
⊢ ∃ x, x ≠ 0 ∧ v x ≠ 1
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
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := ⋯
F_cau : Cauchy (map (⇑i) F)
hi : IsUniformInducing ⇑i
⊢ 𝓝 0 ⊓ map (⇑i) F = ⊥

Tactic:
← Filter.push_pull',

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
⊢ map (⇑i) (Filter.comap (⇑i) (𝓝 0) ⊓ F) = ⊥
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm : (⇑f ∘ fun x ↦ x⁻¹) = (fun x ↦ x⁻¹) ∘ ⇑f
⊢ 𝓝 0 ⊓ map (⇑f) F = ⊥

Tactic:
← Filter.push_pull',

Goal state after:
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm : (⇑f ∘ fun x ↦ x⁻¹) = (fun x ↦ x⁻¹) ∘ ⇑f
⊢ map (⇑f) (Filter.comap (⇑f) (𝓝 0) ⊓ F) = ⊥
Module: Mathlib.RingTheory.Ideal.Oka

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
I : Ideal R
hI : Maximal (fun x ↦ ¬P x) I
⊢ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
by_contra! ⟨a, b, hab, ha, hb⟩
    have h₁ : P (I ⊔ span {a}) := of_not_not <| hI.not_prop_of_gt (Submodule.lt_sup_iff_notMem.2 ha)
    have h₂ : P (I.colon (span {a})) := of_not_not <| hI.not_prop_of_gt <| lt_of_le_of_ne le_colon
      (fun H ↦ hb <| H ▸ mem_colon_span_singleton.2 (mul_comm a b ▸ hab))
    exact hI.prop (hP.oka h₁ h₂)

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

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝ : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
⊢ 0 < v π

Tactic:
rw [IsUniformizer.iff] at hπ

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝ : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v π = ↑(IsRankOneDiscrete.generator v)
⊢ 0 < v π
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Ring R
v : Valuation R Γ₀
S : Type u_3
inst✝¹ : SMul S R
inst✝ : FaithfulSMul S R
m₁✝ m₂✝ : S
h : ∀ (a : WithVal v), m₁✝ • a = m₂✝ • a
⊢ m₁✝ = m₂✝

Tactic:
simp only [smul_right_def, toVal.injEq] at h

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Ring R
v : Valuation R Γ₀
S : Type u_3
inst✝¹ : SMul S R
inst✝ : FaithfulSMul S R
m₁✝ m₂✝ : S
h : ∀ (a : WithVal v), m₁✝ • a.ofVal = m₂✝ • a.ofVal
⊢ m₁✝ = m₂✝
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Ring R
v : Valuation R Γ₀
S : Type u_3
inst✝¹ : SMul S R
inst✝ : FaithfulSMul S R
m₁✝ m₂✝ : S
h : ∀ (a : WithVal v), m₁✝ • a.ofVal = m₂✝ • a.ofVal
⊢ m₁✝ = m₂✝

Tactic:
exact FaithfulSMul.eq_of_smul_eq_smul fun r ↦ h (toVal v r)

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 : K
H : (valuation K (maximalIdeal A)) x ≤ 1
π : A
hπ : Irreducible π
a b : A
hb : b ∈ nonZeroDivisors A
h_frac : (algebraMap A K) a / (algebraMap A K) b = x
ha : a = 0
⊢ ∃ a, (algebraMap A K) a = x

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
H : (valuation K (maximalIdeal A)) x ≤ 1
π : A
hπ : Irreducible π
a b : A
hb : b ∈ nonZeroDivisors A
h_frac : (algebraMap A K) a / (algebraMap A K) b = x
ha : ¬a = 0
⊢ ∃ a, (algebraMap A K) a = x

Tactic:
· rw [← h_frac]
    use 0
    rw [ha, map_zero, zero_div]

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
H : (valuation K (maximalIdeal A)) x ≤ 1
π : A
hπ : Irreducible π
a b : A
hb : b ∈ nonZeroDivisors A
h_frac : (algebraMap A K) a / (algebraMap A K) b = x
ha : ¬a = 0
⊢ ∃ a, (algebraMap A K) a = x
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_4
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
a : G
ha : a ∈ closure {x}
⊢ ∀ {b : ↥(closure {x})},
    { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }.toFun
          ⟨a, ha⟩ ≤
        { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }.toFun
          b ↔
      ⟨a, ha⟩ ≤ b

Tactic:
⟨b, hb⟩

Goal state after:
case refine_4
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
a : G
ha : a ∈ closure {x}
b : G
hb : b ∈ closure {x}
⊢ { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }.toFun
        ⟨a, ha⟩ ≤
      { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }.toFun
        ⟨b, hb⟩ ↔
    ⟨a, ha⟩ ≤ ⟨b, hb⟩