mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case zero
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
⊢ - -zero = zero

pp: case some
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ - -some x✝ y✝ h✝ = some x✝ y✝ h✝

Tactic:
· rfl

Goal state after:
case some
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ - -some x✝ y✝ h✝ = some x✝ y✝ h✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case mp.zero
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
hP : toClass zero = 0
⊢ zero = 0

pp: case mp.some
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x✝ y✝ : F
h : W.Equation x✝ y✝
right✝ : evalEval x✝ y✝ W.polynomialX ≠ 0 ∨ evalEval x✝ y✝ W.polynomialY ≠ 0
hP : toClass (some x✝ y✝ ⋯) = 0
⊢ some x✝ y✝ ⋯ = 0

Tactic:
· rfl

Goal state after:
case mp.some
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x✝ y✝ : F
h : W.Equation x✝ y✝
right✝ : evalEval x✝ y✝ W.polynomialX ≠ 0 ∨ evalEval x✝ y✝ W.polynomialY ≠ 0
hP : toClass (some x✝ y✝ ⋯) = 0
⊢ some x✝ y✝ ⋯ = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

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

Tactic:
ite_not,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (X * (W.preΨ' (n + 1) ^ 2 * if Even n then 1 else W.Ψ₂Sq) -
      W.preΨ ↑(n + 1 + 1) * W.preΨ ↑n * if Even n then W.Ψ₂Sq else 1) =
    (X * W.preΨ' (n + 1) ^ 2 * if Even n then 1 else W.Ψ₂Sq) -
      W.preΨ' (n + 2) * W.preΨ' n * if Even n then W.Ψ₂Sq else 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

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

Tactic:
by
  rw [Φ, add_sub_cancel_right]
  norm_cast
  simp_rw [ΨSq_ofNat, Nat.even_add_one, ite_not, ← mul_assoc, preΨ_ofNat]

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

Goal state before:
pp: case zero.zero
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' : Affine R
inst✝⁸ : DecidableEq F
inst✝⁷ : DecidableEq K
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
h : (map f) zero = (map f) zero
⊢ zero = zero

pp: case some.some
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' : Affine R
inst✝⁸ : DecidableEq F
inst✝⁷ : DecidableEq K
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
x✝¹ y✝¹ : F
h✝¹ : (W'⁄F).Nonsingular x✝¹ y✝¹
x✝ y✝ : F
h✝ : (W'⁄F).Nonsingular x✝ y✝
h : (map f) (some x✝¹ y✝¹ h✝¹) = (map f) (some x✝ y✝ h✝)
⊢ some x✝¹ y✝¹ h✝¹ = some x✝ y✝ h✝

Tactic:
· rfl

Goal state after:
case some.some
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' : Affine R
inst✝⁸ : DecidableEq F
inst✝⁷ : DecidableEq K
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
x✝¹ y✝¹ : F
h✝¹ : (W'⁄F).Nonsingular x✝¹ y✝¹
x✝ y✝ : F
h✝ : (W'⁄F).Nonsingular x✝ y✝
h : (map f) (some x✝¹ y✝¹ h✝¹) = (map f) (some x✝ y✝ h✝)
⊢ some x✝¹ y✝¹ h✝¹ = some x✝ y✝ h✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 3 ≠ 0
⊢ W.Ψ₃.leadingCoeff = 3

Tactic:
by
  rw [leadingCoeff, W.natDegree_Ψ₃ h, coeff_Ψ₃]

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))) *
        ((mk W) (if ¬Even n then W.ψ₂ else 1) * (mk W) (if ¬Even n then W.ψ₂ else 1)) =
    (mk W) (C X) * (mk W) (C (W.ΨSq n)) -
      (mk W) (C (W.preΨ (n + 1))) * (mk W) (C (W.preΨ (n - 1))) * (mk W) (C (if Even n then 1 else W.Ψ₂Sq))

Tactic:
ite_not,

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))) *
        ((mk W) (if Even n then 1 else W.ψ₂) * (mk W) (if Even n then 1 else W.ψ₂)) =
    (mk W) (C X) * (mk W) (C (W.ΨSq n)) -
      (mk W) (C (W.preΨ (n + 1))) * (mk W) (C (W.preΨ (n - 1))) * (mk W) (C (if Even n then 1 else W.Ψ₂Sq))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsElliptic
x : Fin 3 → R
i : Fin 3
⊢ ∑ j, (eval x) (C ↑W.Δ'⁻¹ * W.addSubMapCoeff (i, j)) * (eval x) (W.addSubMap j) = x i ^ 4

Tactic:
simp only [eval_mul, eval_C, mul_assoc]
  rw [← Finset.mul_sum, Units.inv_mul_eq_iff_eq_mul, Fin.sum_univ_three, addSubMap, addSubMapCoeff,
    Function.uncurry_apply_pair, coe_Δ', Δ]
  fin_cases i <;> simp <;> grind only [b_relation]

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

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

Tactic:
linarith only [W.natDegree_preΨ₄ h]

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

Goal state before:
pp: m : ℕ
⊢ ((2 * ↑m + 6) ^ 2 - 4 =
        2 * ((↑m + 2) ^ 2 - if Even m then 4 else 1) + ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
          ((↑m + 5) ^ 2 - if Even m then 1 else 4) ∧
      (2 * ↑m + 6) ^ 2 - 4 =
        ((↑m + 1) ^ 2 - if Even m then 1 else 4) + ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
          2 * ((↑m + 4) ^ 2 - if Even m then 4 else 1)) ∧
    ((2 * ↑m + 4 + 1) ^ 2 - 1 =
        ((↑m + 4) ^ 2 - if Even m then 4 else 1) + 3 * ((↑m + 2) ^ 2 - if Even m then 4 else 1) +
          2 * if Even m then 6 else 0) ∧
      (2 * ↑m + 4 + 1) ^ 2 - 1 =
        ((↑m + 1) ^ 2 - if Even m then 1 else 4) + 3 * ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
          2 * if Even m then 0 else 6

Tactic:
constructor <;> constructor

Goal state after:
case left.left
m : ℕ
⊢ (2 * ↑m + 6) ^ 2 - 4 =
    2 * ((↑m + 2) ^ 2 - if Even m then 4 else 1) + ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
      ((↑m + 5) ^ 2 - if Even m then 1 else 4)

case left.right
m : ℕ
⊢ (2 * ↑m + 6) ^ 2 - 4 =
    ((↑m + 1) ^ 2 - if Even m then 1 else 4) + ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
      2 * ((↑m + 4) ^ 2 - if Even m then 4 else 1)

case right.left
m : ℕ
⊢ (2 * ↑m + 4 + 1) ^ 2 - 1 =
    ((↑m + 4) ^ 2 - if Even m then 4 else 1) + 3 * ((↑m + 2) ^ 2 - if Even m then 4 else 1) +
      2 * if Even m then 6 else 0

case right.right
m : ℕ
⊢ (2 * ↑m + 4 + 1) ^ 2 - 1 =
    ((↑m + 1) ^ 2 - if Even m then 1 else 4) + 3 * ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
      2 * if Even m then 0 else 6
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✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJEqZeroNF
inst✝ : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero 3
u : F
hu : u ^ 3 = E.a₃ / E'.a₃
s : F
hs : 1 * s ^ 4 + E.a₃ * s + (E.a₄ - u ^ 4 * E'.a₄) = 0
t : F
ht : 1 * t ^ 2 + E.a₃ * t + (s ^ 6 + E.a₄ * s ^ 2 + E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ ({ u := Units.mk0 u hu0, r := s ^ 2, s := s, t := t } • E).a₃ = E'.a₃

Tactic:
simp_rw [variableChange_a₃, Units.val_inv_eq_inv_val, Units.val_mk0, inv_pow, inv_mul_eq_div,
      hu, a₁_of_isCharTwoJEqZeroNF, show (2 : F) = 0 from CharP.cast_eq_zero F 2]

Goal state after:
case h.a₃
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJEqZeroNF
inst✝ : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero 3
u : F
hu : u ^ 3 = E.a₃ / E'.a₃
s : F
hs : 1 * s ^ 4 + E.a₃ * s + (E.a₄ - u ^ 4 * E'.a₄) = 0
t : F
ht : 1 * t ^ 2 + E.a₃ * t + (s ^ 6 + E.a₄ * s ^ 2 + E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ (E.a₃ + s ^ 2 * 0 + 0 * t) / (E.a₃ / E'.a₃) = E'.a₃
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_1
I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
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)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
i' : I
fi'i : i' ⟶ i
hi' : ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2
𝒱' : ↥s → (D.obj i').Opens := fun x ↦ D.map fi'i ⁻¹ᵁ 𝒱 x
h𝒱'𝒰 : ∀ (j : ↥s), c.π.app i' ⁻¹ᵁ 𝒱' j = (↑↑j).1
x✝ : ∀ (j : ↥s) (k : Over i'), IsAffine ((opensDiagram D i' (𝒱' j)).obj k)
t𝒱 : (j : ↥s) → opensDiagram D i' (𝒱' j) ⟶ (Functor.const (Over i')).obj ↑↑(↑(↑↑j).2).2 :=
  fun j ↦ { app := fun k ↦ Hom.resLE (t.app k.left) (↑(↑(↑↑j).2).2) (D.map k.hom ⁻¹ᵁ 𝒱' j) ⋯, naturality := ⋯ }
this : ∀ (j : ↥s), IsAffine ↑(↑(↑↑j).2).1
k : ↥s → Over i'
ak : (j : ↥s) → (opensDiagram D i' (𝒱' j)).obj (k j) ⟶ ↑(↑(↑↑j).2).1
hk : ∀ (j : ↥s), (opensCone D c i' (𝒱' j)).π.app (k j) ≫ ak j = Hom.resLE a (↑(↑↑j).2).1 (c.π.app i' ⁻¹ᵁ 𝒱' j) ⋯
hk' : ∀ (j : ↥s), ak j ≫ Hom.resLE f (↑(↑(↑↑j).2).2) (↑(↑↑j).2).1 ⋯ = (t𝒱 j).app (k j)
i'' : I
fi''i' : i'' ⟶ i'
fi'' : (x : ↥s) → i'' ⟶ (k x).left
hi'' : ∀ (x : ↥s), fi'' x ≫ (k x).hom = fi''i'
j : ↥s
⊢ D.map (fi''i' ≫ fi'i) ⁻¹ᵁ 𝒱 j ≤ D.map (fi'' j) ⁻¹ᵁ D.map (k j).hom ⁻¹ᵁ 𝒱' j

Tactic:
simp only [← Hom.comp_preimage, ← Functor.map_comp, 𝒱', reassoc_of% hi'']; rfl

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.Nonsingular P ↔ W'.Nonsingular Q

Tactic:
rcases h with ⟨u, rfl⟩
  exact nonsingular_smul Q u.isUnit

Goal state after:
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 (-(P y / P x) • ![1, 1, 0]) = -toAffine W P

Tactic:
toAffine_smul _ ((isUnit_Y_of_Z_eq_zero hP hPz).div <| isUnit_X_of_Z_eq_zero hP hPz).neg,

Goal state after:
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 ![1, 1, 0] = -toAffine W P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Tactic:
rw [toAffine_of_Z_eq_zero hPz, zero_add]
    by_cases hQz : Q z = 0
    · rw [add_of_Z_eq_zero hP hQ hPz hQz, toAffine_smul _ <| (isUnit_X_of_Z_eq_zero hP hPz).pow 2,
        toAffine_zero, toAffine_of_Z_eq_zero hQz]
    · rw [add_of_Z_eq_zero_left hP.left hPz hQz,
        toAffine_smul _ <| (isUnit_X_of_Z_eq_zero hP hPz).mul <| Ne.isUnit hQz]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y z : R
⊢ x * y * z =ᵥ x * z * y

Tactic:
by
  grw [mul_assoc, veq_mul_comm y, mul_assoc]

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)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
⊢ ValueGroupWithZero.mk (x ^ n) (s ^ n) = ValueGroupWithZero.mk (y ^ n) (t ^ n)

Tactic:
induction n with
    | zero => simp
    | succ n ih =>
      simp only [pow_succ, ← ValueGroupWithZero.mk_mul_mk, ih]
      apply congrArg (_ * ·)
      exact ValueGroupWithZero.sound h₁ h₂

Goal state after:
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:
rw [Valuation.map_mul, Hx, mul_comm]

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 y * ↑γx < ↑((Units.map ↑embedding) γ)
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
γ : (ofClass v).ValueGroup₀ˣ
⊢ True ∧ ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ)) ⊆ s ↔ {x | v x < embedding ↑γ} ⊆ s

Tactic:
rw [true_and]

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
γ : (ofClass v).ValueGroup₀ˣ
⊢ ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ)) ⊆ s ↔ {x | v x < embedding ↑γ} ⊆ s
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
a b c : ValueGroupWithZero R
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ c

Tactic:
induction a using ValueGroupWithZero.ind with | mk a₁ a₂
    induction b using ValueGroupWithZero.ind with | mk b₁ b₂
    induction c using ValueGroupWithZero.ind with | mk c₁ c₂
    rw [ValueGroupWithZero.mk_le_mk] at hab hbc ⊢
    apply vle_mul_cancel b₂.prop
    calc a₁ * c₂ * b₂
      _ =ᵥ a₁ * b₂ * c₂ := by grw [veq_mul_right_comm]
      _ ≤ᵥ b₁ * a₂ * c₂ := mul_vle_mul_left hab _
      _ =ᵥ b₁ * c₂ * a₂ := by grw [veq_mul_right_comm]
      _ ≤ᵥ c₁ * b₂ * a₂ := mul_vle_mul_left hbc _
      _ =ᵥ c₁ * a₂ * b₂ := by grw [veq_mul_right_comm]

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

Goal state before:
pp: M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : UniformSpace α
inst✝³ : MonoidWithZero M
inst✝² : Zero α
inst✝¹ : MulActionWithZero M α
inst✝ : UniformContinuousConstSMul M α
r : M
⊢ r • 0 = 0

Tactic:
rw [← coe_zero, ← coe_smul, MulActionWithZero.smul_zero r]

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

Goal state before:
pp: α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
x y : α
⊢ (inseparableSetoid α) x y ↔ (Submodule.quotientRel ⊥.closure) x y

Tactic:
inseparableSetoid_ring

Goal state after:
α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
x y : α
⊢ (Submodule.quotientRel ⊥.closure) x y ↔ (Submodule.quotientRel ⊥.closure) x y
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
⊢ Relator.LiftFun (⇑(inseparableSetoid α)) (⇑(Submodule.quotientRel ⊥.closure)) id id

Tactic:
inseparableSetoid_ring

Goal state after:
α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
⊢ Relator.LiftFun (⇑(Submodule.quotientRel ⊥.closure)) (⇑(Submodule.quotientRel ⊥.closure)) id id
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
⊢ Relator.LiftFun (⇑(Submodule.quotientRel ⊥.closure)) (⇑(inseparableSetoid α)) id id

Tactic:
inseparableSetoid_ring

Goal state after:
α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
⊢ Relator.LiftFun (⇑(Submodule.quotientRel ⊥.closure)) (⇑(Submodule.quotientRel ⊥.closure)) id id
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 := K.subtype
F_cau : Cauchy (map (⇑i) F)
hi : IsUniformInducing ⇑i
⊢ map ⇑i ⊥ = ⊥

Tactic:
Filter.map_bot

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
⊢ ⊥ = ⊥
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
⊢ map ⇑f ⊥ = ⊥

Tactic:
Filter.map_bot

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
⊢ ⊥ = ⊥
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
⊢ generator v = Units.mk0 (exp (-1)) generator_eq_exp_neg_one_of_mem_range._proof_1

Tactic:
rw [← Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator]

Goal state after:
A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hπ : exp (-1) ∈ range ⇑v
⊢ Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup =
    Units.mk0 (exp (-1)) generator_eq_exp_neg_one_of_mem_range._proof_1
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
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer ↑π₁
h2 : v.IsUniformizer ↑π₂
⊢ Associated π₁ π₂

Tactic:
by
  have hval : v ((π₁ : K)⁻¹ * π₂) = 1 := by
    simp [IsUniformizer.iff.mp h1, IsUniformizer.iff.mp h2]
  set p : v.integer := ⟨(π₁.1 : K)⁻¹ * π₂.1, (v.mem_integer_iff _).mpr (le_of_eq hval)⟩ with hp
  use ((Integers.isUnit_iff_valuation_eq_one (x := p) <| integer.integers v).mpr hval).unit
  apply_fun ((↑) : K₀ → K) using Subtype.val_injective
  simp [hp, ← mul_assoc, mul_inv_cancel₀ h1.ne_zero]

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
y : R := (equiv v) x
hy : toVal v y = x
hs0' : 0 < Valued.v.restrict (toVal v s)
h' : v.restrict.IsEquiv w.restrict
hx : Valued.v.restrict x * Valued.v.restrict (toVal v s) < Valued.v.restrict (toVal v r)
⊢ v (y * s) < v r

Tactic:
rwa [← map_mul, restrict_lt_iff] at hx

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

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : v (x - y) < min (↑γ * (v y * v y)) (v y)
⊢ v (x⁻¹ - y⁻¹) < ↑γ

Tactic:
have hyp1 : v (x - y) < γ * (v y * v y) := lt_of_lt_of_le h (min_le_left _ _)

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
⊢ v (x⁻¹ - y⁻¹) < ↑γ
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
hcomp : WithVal.congr v w (RingEquiv.refl R) = WithVal.congr v w (RingEquiv.refl R)
h1 : UniformContinuous ⇑(equiv v)
h2 : UniformContinuous ⇑(equiv w).symm
hR : UniformContinuous ⇑(RingHom.id R)
⊢ UniformContinuous ⇑(WithVal.congr v w (RingEquiv.refl R))

Tactic:
apply @UniformContinuous.comp (WithVal v) R (WithVal w) _ (Valued.mk' w).toUniformSpace _
    ((RingEquiv.refl R).trans (WithVal.equiv w).symm) (WithVal.equiv v) ?_ h1

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 Γ₀'
h : v.IsEquiv w
hcomp : WithVal.congr v w (RingEquiv.refl R) = WithVal.congr v w (RingEquiv.refl R)
h1 : UniformContinuous ⇑(equiv v)
h2 : UniformContinuous ⇑(equiv w).symm
hR : UniformContinuous ⇑(RingHom.id R)
⊢ UniformContinuous ⇑((RingEquiv.refl R).trans (equiv w).symm)
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mp.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ha✝ : a ≠ 1
ha : a < 1
⊢ Function.Injective fun x ↦ a ^ x

Tactic:
exact (zpow_right_strictAnti ha).injective

Goal state after: