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

Goal state before:
pp: X Y S : Scheme
inst✝⁴ : IsAffine X
inst✝³ : IsAffine Y
π : X ⟶ Y
inst✝² : Surjective π
inst✝¹ : Flat π
f : X ⟶ S
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
inst✝ : IsAffine S
⊢ ∃ u, π ≫ u = f

Tactic:
have : EffectiveEpi (AffineScheme.ofHom π) := by
    apply AffineScheme.equivCommRingCat.functor.effectiveEpi_of_map
    apply CommRingCat.Opposite.effectiveEpi_of_faithfullyFlat
    exact (Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine π).mp ⟨‹_›, ‹_›⟩
  obtain ⟨u, hu⟩ := IsRegularEpi.exists_of_isKernelPair
    (AffineScheme.ofHom π)
    (IsPullback.of_map (f := AffineScheme.ofHom (pullback.fst π π)) (AffineScheme.forgetToScheme)
      (InducedCategory.Hom.ext pullback.condition) (.of_hasPullback _ _))
    (AffineScheme.ofHom f) (InducedCategory.Hom.ext hf)
  use u.hom, InducedCategory.Hom.ext_iff.mp hu

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.a₃ ^ 2 + 4 * W.a₆ = W.a₃ ^ 2

Tactic:
linear_combination 2 * W.a₆ * CharP.cast_eq_zero R 2

Goal state after:
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)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this✝¹ : CompactSpace ↥c.pt
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : (c.π.app i) x ∈ ↑U
this✝ : ∀ (j : Over i), IsAffine ((opensDiagram D i U).obj j)
j : Over i
t : ↑Γ((opensDiagram D i U).obj j, ⊤)
hj :
  (ConcreteCategory.hom (Scheme.Hom.appTop ((opensCone D c i U).π.app j))) t =
    (s |_ ⋯.functor.obj (Opposite.unop (Opposite.op ⊤))) ⋯
this : (c.π.app j.left ≫ D.map j.hom) x ∈ U
⊢ (c.π.app j.left) x ∈ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤

Tactic:
simpa [-Cone.w] using this

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

Goal state before:
pp: case neg
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
hx : ¬x₁ = x₂
⊢ W.Nonsingular x₂ (y₂ - y₁ + y₁)

Tactic:
sub_add_cancel

Goal state after:
case neg
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
hx : ¬x₁ = x₂
⊢ W.Nonsingular x₂ y₂
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b : ℤ
⊢ -(W ((a + b).tdiv 2) * W ((a - b).tdiv 2)) = W ((b + a).tdiv 2) * W ((b - a).tdiv 2)

Tactic:
add_comm,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b : ℤ
⊢ -(W ((b + a).tdiv 2) * W ((a - b).tdiv 2)) = W ((b + a).tdiv 2) * W ((b - a).tdiv 2)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c : ℤ
⊢ W a * W 0 * atom W b c - atom W a c * atom W a b + atom W a c * atom W a b = W a * W 0 * atom W b c

Tactic:
sub_add_cancel

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c : ℤ
⊢ atom W a b * (W c * W 0) - atom W a c * atom W b c + atom W a c * atom W b c = atom W a b * (W c * W 0)

Tactic:
sub_add_cancel

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
⊢ atomRel W (2 * a) (2 * b) (2 * c) (2 * d) =
    atomRel W (2 * a - 2 * d + 2 * d) (2 * b - 2 * d + 2 * d) (2 * c - 2 * d + 2 * d) (2 * d)

Tactic:
sub_add_cancel

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
h : IsEllipticNet W
x : R
p q r s : ℤ
⊢ rel (x • W) p q r s + x ^ 4 * 0 - (0 + x ^ 4 * rel W p q r s) = 0

Tactic:
(simp_rw [rel, Pi.smul_apply, smul_eq_mul]; ring1)

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ complEDS₂ b c d (-k) = complEDS₂ b c d k

Tactic:
by
  simp_rw [complEDS₂, ← neg_add', ← sub_neg_eq_add, ← neg_sub', preNormEDS_neg, even_neg]
  ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Φ 4 = X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)

Tactic:
rw [show 4 = ((3 : ℕ) + 1 : ℤ) by rfl, Φ_ofNat, preΨ'_four, if_neg <| by decide,
    show 3 + 2 = 2 * 2 + 1 by rfl, preΨ'_odd, preΨ'_four, preΨ'_two, if_pos Even.zero, preΨ'_one,
    preΨ'_three, if_pos Even.zero, if_neg <| by decide]

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.Ψ₃ ^ 3 * 1) * W.Ψ₃ * 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
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ preNormEDS ((mk W) (W.ψ₂ ^ 4)) ((mk W) (C W.Ψ₃)) ((mk W) (C W.preΨ₄)) n * (mk W) (if Even n then W.ψ₂ else 1) =
    preNormEDS ((mk W) (C (W.Ψ₂Sq ^ 2))) ((mk W) (C W.Ψ₃)) ((mk W) (C W.preΨ₄)) n * (mk W) (if Even n then W.ψ₂ else 1)

Tactic:
map_pow,

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

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (mk W) (C X) * (mk W) (W.ψ n) ^ 2 - (mk W) (W.ψ (n + 1)) * (mk W) (W.ψ (n - 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))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (mk W) (W.φ n) = (mk W) (C (W.Φ n))

Tactic:
simp_rw [φ, Φ, map_sub, map_mul, map_pow, mk_ψ, mk_Ψ_sq, Ψ, map_mul,
    mul_mul_mul_comm _ <| mk W <| ite .., Int.even_add_one, Int.even_sub_one, ite_not, ← sq,
    apply_ite C, apply_ite <| mk W, ite_pow, map_one, one_pow, mk_ψ₂_sq]

Goal state after:
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 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
⊢ u ≠ 0

Tactic:
← pow_ne_zero_iff three_ne_zero,

Goal state after:
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
⊢ u ^ 3 ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ 4 * W.a₆ = 0

Tactic:
linear_combination 2 * W.a₆ * CharP.cast_eq_zero R 2

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ W'.polynomialY = C 2 * Y + C W'.a₁ * X * Z + C W'.a₃ * Z ^ 3

Tactic:
rw [polynomialY, polynomial]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ (pderiv y)
      (Y ^ 2 + C W'.a₁ * X * Y * Z + C W'.a₃ * Y * Z ^ 3 -
        (X ^ 3 + C W'.a₂ * X ^ 2 * Z ^ 2 + C W'.a₄ * X * Z ^ 4 + C W'.a₆ * Z ^ 6)) =
    C 2 * Y + C W'.a₁ * X * Z + C W'.a₃ * Z ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = ↑(if Even ↑n then ↑n / 2 else ↑n)
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:
| neg ih n =>

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

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

Tactic:
| neg ih n =>

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

Goal state before:
pp: case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), 2 < (↑n).natAbs → ↑↑n ≠ 0 → 0 < (W.preΨ ↑n).natDegree
n : ℕ
hn : 2 < (-↑n).natAbs
h : ↑(-↑n) ≠ 0
⊢ 0 < (W.preΨ (-↑n)).natDegree

Tactic:
| neg ih n =>

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
ih : ∀ (n : ℕ), ↑↑n ≠ 0 → W.preΨ ↑n ≠ 0
n : ℕ
h : ↑(-↑n) ≠ 0
⊢ W.preΨ (-↑n) ≠ 0

Tactic:
| neg ih n =>

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

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

Tactic:
have hu4 : u ^ 4 = E.a₄ / E'.a₄ := by
    rw [pow_mul u 2 2, hu]
    simp [field]
    linear_combination -heq

Goal state after:
case neg
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : u ^ 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : u ^ 4 = E.a₄ / E'.a₄
⊢ ∃ C, C • E = E'
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
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
⊢ W.toAffine.negY
      (W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
        (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)))
      (![W.dblX P, W.negDblY P, W.dblZ P] y / ![W.dblX P, W.negDblY P, W.dblZ P] z ^ 3) =
    W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
      (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))

Tactic:
negDblY_of_Z_ne_zero hP hQ hPz hQz hx hy,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
⊢ W.toAffine.negY
      (W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
        (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)))
      (W.toAffine.negAddY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
        (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))) =
    W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
      (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))
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
⊢ s ∈ 𝓝 a ↔ ∃ i, True ∧ {b | b - a ∈ B i} ⊆ s

Tactic:
(hB.toRingFilterBasis.toAddGroupFilterBasis.nhds_hasBasis a).mem_iff

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 ∈ hB.toRingFilterBasis.toAddGroupFilterBasis, (fun y ↦ a + y) '' i ⊆ s) ↔ ∃ i, True ∧ {b | b - a ∈ B i} ⊆ s
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z = 0
⊢ toAffine W P = 0

Tactic:
by
  rw [toAffine, dif_neg <| not_and_not_right.mpr fun _ => hPz]

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

Goal state before:
pp: K : Type u
inst✝² : DivisionRing K
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : MulArchimedean Γ₀
v : Valuation K Γ₀
r : Γ₀
hr : r ≠ 0
h : ∀ (x : K), v x ≠ 0 → r < v x
x : K
hx : v x ≠ 0
⊢ v x = 1

Tactic:
lift r to Γ₀ˣ using IsUnit.mk0 _ hr

Goal state after:
K : Type u
inst✝² : DivisionRing K
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : MulArchimedean Γ₀
v : Valuation K Γ₀
x : K
hx : v x ≠ 0
r : Γ₀ˣ
hr : ↑r ≠ 0
h : ∀ (x : K), v x ≠ 0 → ↑r < v x
⊢ v x = 1
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: case inr
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) ⋯
⊢ ∃ j,
    ↑(v.ltAddSubgroup ((Units.map ↑embedding) j)) ⊆
      (fun x_1 ↦ x_1 * x) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))

Tactic:
have hu : ValueGroup₀.embedding u⁻¹.1 = γx⁻¹ := by simp [restrict₀_apply, embedding_apply,
          hu_def, Hx]

Goal state after:
case inr
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⁻¹
⊢ ∃ j,
    ↑(v.ltAddSubgroup ((Units.map ↑embedding) j)) ⊆
      (fun x_1 ↦ x_1 * x) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: case mp
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
h : ∀ (U : Set R), (∃ i, U = ↑(v.ltAddSubgroup ((Units.map ↑embedding) i))) → ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ

Tactic:
γ

Goal state after:
case mp
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
h : ∀ (U : Set R), (∃ i, U = ↑(v.ltAddSubgroup ((Units.map ↑embedding) i))) → ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
γ : (ofClass v).ValueGroup₀ˣ
⊢ ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : TopologicalSpace R
inst✝ : IsValuativeTopology R
x : R
⊢ (𝓝 x).HasBasis (fun x ↦ True) fun γ ↦ {z | (valuation R) (z - x) < ↑γ}

Tactic:
simp [Filter.hasBasis_iff, mem_nhds_iff']

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

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
x : ↥(posSubmonoid R)
⊢ (valuation R) ↑x ≠ 0

Tactic:
rw [ne_eq, valuation_eq_zero_iff]

Goal state after:
R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
x : ↥(posSubmonoid R)
⊢ ¬↑x ≤ᵥ 0
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case mp
R : Type u_1
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst✝² : IsUniformAddGroup R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
F : Filter R
h : ∀ (U : Set R), (∃ i, U = ↑(v.ltAddSubgroup ((Units.map ↑embedding) i))) → ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ

Tactic:
γ

Goal state after:
case mp
R : Type u_1
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst✝² : IsUniformAddGroup R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
F : Filter R
h : ∀ (U : Set R), (∃ i, U = ↑(v.ltAddSubgroup ((Units.map ↑embedding) i))) → ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
γ : (ofClass v).ValueGroup₀ˣ
⊢ ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ
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✝¹ : AddGroup α
inst✝ : IsUniformAddGroup α
a✝ : Completion α
a : α
⊢ -↑a + ↑a = 0

Tactic:
rw_mod_cast [neg_add_cancel]
        rfl

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

Goal state before:
pp: α : Type u_1
inst✝⁹ : Ring α
inst✝⁸ : UniformSpace α
inst✝⁷ : IsTopologicalRing α
inst✝⁶ : IsUniformAddGroup α
β : Type u
inst✝⁵ : UniformSpace β
inst✝⁴ : Ring β
inst✝³ : IsUniformAddGroup β
inst✝² : IsTopologicalRing β
f : α →+* β
hf✝ : Continuous ⇑f
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
hf' : Continuous ⇑↑f
hf : UniformContinuous ⇑f
⊢ Completion.extension (⇑f) 1 = 1

Tactic:
rw [← coe_one, extension_coe hf, f.map_one]

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
x y : β
a b : α
⊢ ⋯.extend (⇑f) (i a * i b) = ⋯.extend (⇑f) (i a) * ⋯.extend (⇑f) (i b)

Tactic:
simp_rw [← i.map_mul, IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous _,
        ← f.map_mul]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Oka

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hchain : ∀ C ⊆ {I | ¬P I}, IsChain (fun x1 x2 ↦ x1 ≤ x2) C → ∀ x ∈ C, P (sSup C) → ∃ I ∈ C, P I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
I : Ideal R
hI : ¬P I
C : Set (Ideal R)
hC₁ : C ⊆ {I | ¬P I}
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) C
J : Ideal R
hJ : J ∈ C
⊢ sSup C ∈ {I | ¬P I}

Tactic:
intro H

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hchain : ∀ C ⊆ {I | ¬P I}, IsChain (fun x1 x2 ↦ x1 ≤ x2) C → ∀ x ∈ C, P (sSup C) → ∃ I ∈ C, P I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
I : Ideal R
hI : ¬P I
C : Set (Ideal R)
hC₁ : C ⊆ {I | ¬P I}
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) C
J : Ideal R
hJ : J ∈ C
H : P (sSup C)
⊢ False
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R✝ : Type u_1
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
⊢ ↑(ofClass Valued.v).valueGroup = ↑(ofClass v).valueGroup

Tactic:
by simp [valueGroup_eq v]

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

Goal state before:
pp: case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation (π ^ n) / (maximalIdeal A).intValuation ↑⟨π ^ m, hb⟩ ≤ 1
⊢ ∃ a, (algebraMap A K) a = x

Tactic:
map_pow,

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_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation ↑⟨π ^ m, hb⟩ ≤ 1
⊢ ∃ a, (algebraMap A K) a = x
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
x_ne : x ≠ 0
s : Set K
s_in : s ∈ 𝓝 x⁻¹
⊢ s ∈ map Inv.inv (𝓝 x)

Tactic:
by
      obtain ⟨γ, hs⟩ := Valued.mem_nhds.mp s_in; clear s_in
      rw [mem_map, Valued.mem_nhds]
      let γ' := Units.mk0 ((ValueGroup₀.restrict₀ _) x) (v.restrict.ne_zero_iff.mpr x_ne)
      use min (γ * (γ' * γ')) γ'
      intro y y_in
      apply hs
      simp only [mem_ofPred_eq, Units.min_val, Units.val_mul] at y_in
      exact Valuation.inversion_estimate _ x_ne y_in

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 y : K
h : (valuation K (maximalIdeal A)) x = (valuation K (maximalIdeal A)) y
hx : x = 0
⊢ ∃ u, u • x = y

Tactic:
eq_comm

Goal state after:
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 y : K
h : (valuation K (maximalIdeal A)) y = (valuation K (maximalIdeal A)) x
hx : x = 0
⊢ ∃ u, u • x = y