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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ -(4 * W.a₂) ^ 3 + 36 * (4 * W.a₂) * (2 * W.a₄) - 216 * W.b₆ = -64 * W.a₂ ^ 3 + 288 * W.a₂ * W.a₄ - 864 * W.a₆

Tactic:
b₆_of_isCharNeTwoNF

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ -(4 * W.a₂) ^ 3 + 36 * (4 * W.a₂) * (2 * W.a₄) - 216 * (4 * W.a₆) = -64 * W.a₂ ^ 3 + 288 * W.a₂ * W.a₄ - 864 * W.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.Δ = -64 * W.a₂ ^ 3 * W.a₆ + 16 * W.a₂ ^ 2 * W.a₄ ^ 2 - 64 * W.a₄ ^ 3 - 432 * W.a₆ ^ 2 + 288 * W.a₂ * W.a₄ * W.a₆

Tactic:
rw [Δ, b₂_of_isCharNeTwoNF, b₄_of_isCharNeTwoNF, b₆_of_isCharNeTwoNF, b₈_of_isCharNeTwoNF]
  ring1

Goal state after:
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).ΨSq n = Polynomial.map (↑f) ((W⁄A).ΨSq n)

Tactic:
← map_ΨSq,

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).ΨSq n = ((W⁄A).map ↑f).ΨSq n
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: 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
j : ↥s
k : Over i'
⊢ ((opensCone D c i' (𝒱' j)).π ≫ t𝒱 j).app k =
    ((Functor.const (Over i')).map
          (Hom.resLE a (↑(↑↑j).2).1 (c.π.app i' ⁻¹ᵁ 𝒱' j) ⋯ ≫ Hom.resLE f (↑(↑(↑↑j).2).2) (↑(↑↑j).2).1 ⋯)).app
      k

Tactic:
simp [t𝒱, Hom.resLE_comp_resLE, show c.π.app k.left ≫ t.app k.left = a ≫ f from
        congr(($ha).app k.left)]

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 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero 2
u : F
hu : u ^ 2 = E.a₂ / E'.a₂
⊢ u ≠ 0

Tactic:
← pow_ne_zero_iff two_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 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero 2
u : F
hu : u ^ 2 = E.a₂ / E'.a₂
⊢ u ^ 2 ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

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

Tactic:
rw [coeff_preΨ', if_pos <| even_two_mul n, n.mul_div_cancel_left two_pos]
    exact right_ne_zero_of_mul <| by rwa [← Nat.cast_mul]

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
heq : E.j = E'.j
p : ℕ
h✝ : CharP F p
⊢ ∃ C, C • E = E'

Tactic:
by_cases hchar2 : p = 2

Goal state after:
case pos
F : Type u_1
inst✝³ : Field F
inst✝² : IsSepClosed F
E E' : WeierstrassCurve F
inst✝¹ : E.IsElliptic
inst✝ : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h✝ : CharP F p
hchar2 : p = 2
⊢ ∃ C, C • E = E'

case neg
F : Type u_1
inst✝³ : Field F
inst✝² : IsSepClosed F
E E' : WeierstrassCurve F
inst✝¹ : E.IsElliptic
inst✝ : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h✝ : CharP F p
hchar2 : ¬p = 2
⊢ ∃ 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.dblU P ^ 2 - W.a₁ * W.dblU P * P z * (P y - W.negY P) - W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 -
        2 * P x * (P y - W.negY P) ^ 2) /
      W.dblZ P ^ 2 =
    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))

Tactic:
toAffine_slope_of_eq 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.dblU P ^ 2 - W.a₁ * W.dblU P * P z * (P y - W.negY P) - W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 -
        2 * P x * (P y - W.negY P) ^ 2) /
      W.dblZ P ^ 2 =
    W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (-W.dblU P / W.dblZ P)
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.dblU P *
          (W.dblU P ^ 2 - W.a₁ * W.dblU P * P z * (P y - W.negY P) - W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 -
              2 * P x * (P y - W.negY P) ^ 2 -
            P x * (P y - W.negY P) ^ 2) +
        P y * (P y - W.negY P) ^ 3) /
      W.dblZ P ^ 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))

Tactic:
toAffine_slope_of_eq 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.dblU P *
          (W.dblU P ^ 2 - W.a₁ * W.dblU P * P z * (P y - W.negY P) - W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 -
              2 * P x * (P y - W.negY P) ^ 2 -
            P x * (P y - W.negY P) ^ 2) +
        P y * (P y - W.negY P) ^ 3) /
      W.dblZ P ^ 3 =
    W.toAffine.negAddY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (-W.dblU P / W.dblZ P)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

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

Tactic:
rw [addU, hPz, zero_mul, div_zero, neg_zero]

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

Goal state before:
pp: case inr.inr
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
H : 1 < Units.mk0 (v x) hx
⊢ v x = 1

Tactic:
rw [← inv_lt_one'] at H
    obtain ⟨k, hk⟩ := exists_pow_lt H r
    specialize h (x ^ (-k : ℤ)) (by simp [hx])
    simp only [zpow_neg, zpow_natCast, map_inv₀, map_pow] at h
    simp [← Units.val_lt_val, h.not_gt, inv_pow] at hk

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
a b c : ValueGroupWithZero R
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ c

Tactic:
induction a using ValueGroupWithZero.ind with | mk a₁ a₂
     =>  _ 

Goal state after:
case mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
b c : ValueGroupWithZero R
hbc : b ≤ c
a₁ : R
a₂ : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk a₁ a₂ ≤ b
⊢ ValueGroupWithZero.mk a₁ a₂ ≤ c
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 Γ₀
_u : UniformSpace R
inst✝² : IsUniformAddGroup R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
F : Filter R
⊢ (∀ U ∈ ⋯.toRingFilterBasis.toAddGroupFilterBasis, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) ↔
    ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ

Tactic:
v.subgroups_basis.mem_addGroupFilterBasis_iff

Goal state after:
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
⊢ (∀ (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: case refine_1
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : IsUniformAddGroup β
x : Completion α
⊢ Continuous ⇑0

Tactic:
exact continuous_const

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} \ {x | v.restrict x < r})

Tactic:
exact IsClopen.diff (isClopen_closedBall hr) (isClopen_ball _)

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 : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ embedding ((embed v) ((valuation R) a)) * embedding ((embed v) ((valuation R) ↑s)) <
    embedding ((embed v) ((valuation R) b)) * embedding ((embed v) ((valuation R) ↑r))

pp: case hb
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ 0 < embedding ((embed v) ((valuation R) ↑r))

pp: case hd
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ 0 < embedding ((embed v) ((valuation R) ↑s))

pp: case hb
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a / (valuation R) ↑r < (valuation R) b / (valuation R) ↑s
⊢ 0 < (valuation R) ↑r

pp: case hd
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a / (valuation R) ↑r < (valuation R) b / (valuation R) ↑s
⊢ 0 < (valuation R) ↑s

Tactic:
any_goals simp only [zero_lt_iff, ne_eq, Valuation.apply_posSubmonoid_ne_zero, not_false_eq_true]

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 : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ embedding ((embed v) ((valuation R) a)) * embedding ((embed v) ((valuation R) ↑s)) <
    embedding ((embed v) ((valuation R) b)) * embedding ((embed v) ((valuation R) ↑r))

case hb
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ ¬embedding ((embed v) ((valuation R) ↑r)) = 0

case hd
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ ¬embedding ((embed v) ((valuation R) ↑s)) = 0
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
⊢ Function.Injective fun x ↦ embedding (⋯.orderMonoidIso x)

Tactic:
rw [← Function.comp_def, EquivLike.injective_comp]

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
⊢ Function.Injective ⇑embedding
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : ValuativeRel A
inst✝² : ValuativeRel B
inst✝¹ : Algebra A B
inst✝ : ValuativeExtension A B
a b : A
⊢ ¬b ≤ᵥ a ↔ a <ᵥ b

Tactic:
not_vle

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : ValuativeRel A
inst✝² : ValuativeRel B
inst✝¹ : Algebra A B
inst✝ : ValuativeExtension A B
a b : A
⊢ a <ᵥ b ↔ a <ᵥ b
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ ![((u * v) ^ 2) ^ 2 * W'.addX P Q, ((u * v) ^ 2) ^ 3 * W'.addY P Q, addZ (u • P) (v • Q)] =
    (u * v) ^ 2 • W'.addXYZ P Q

Tactic:
addZ_smul,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ ![((u * v) ^ 2) ^ 2 * W'.addX P Q, ((u * v) ^ 2) ^ 3 * W'.addY P Q, (u * v) ^ 2 * addZ P Q] =
    (u * v) ^ 2 • W'.addXYZ P Q
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case h
Γ : 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 : Γˣ := ⋯
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 := ⋯
ha : a = ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha₀ : ↑a ≠ 0
h_unit_a : IsUnit a
⊢ ↑r = ↑(π.val ^ n) * ↑↑h_unit_a.unit

Tactic:
rw [IsUnit.unit_spec, Subring.coe_pow, ha, ← mul_assoc, zpow_neg, hn, zpow_natCast,
    mul_inv_cancel₀ (pow_ne_zero _ π.ne_zero), one_mul]

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 : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
x : R
hx : v x * v s.ofVal < v r.ofVal
⊢ Valued.v.restrict (toVal v x) < ↑γ

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 : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
x : R
hx : Valued.v.restrict x < Valued.v.restrict r.ofVal / Valued.v.restrict s.ofVal
⊢ 0 < Valued.v.restrict s.ofVal

Tactic:
· rw [← hr, lt_div_iff₀ ((restrict_pos_iff Valued.v s).mpr hs₀), ← map_mul, ← lt_def,
      ← h.orderRingIso_apply]
    simp only [orderRingIso_apply, toVal_mul, lt_def, ofVal_mul, restrict_lt_iff]
    rw [map_mul]
    exact hx

Goal state after:
case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
x : R
hx : Valued.v.restrict x < Valued.v.restrict r.ofVal / Valued.v.restrict s.ofVal
⊢ 0 < Valued.v.restrict s.ofVal
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithTop X)
⊢ DenselyOrdered ↑s ↔ s.Subsingleton

Tactic:
have he : StrictAnti (WithTop.toDual.image s) :=
    WithTop.toDual.image_strictAnti _ (fun ⦃a b⦄ a ↦ a)

Goal state after:
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithTop X)
he : StrictAnti ⇑(WithTop.toDual.image s)
⊢ DenselyOrdered ↑s ↔ s.Subsingleton
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: 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
⊢ Subring.map (algebraMap A K) ⊤ = (valuation K (maximalIdeal A)).valuationSubring.toSubring

Tactic:
ext
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · obtain ⟨_, _, rfl⟩ := Subring.mem_map.mp h
    apply valuation_le_one
  · obtain ⟨y, rfl⟩ := exists_lift_of_le_one h
    rw [Subring.mem_map]
    exact ⟨y, mem_top _, rfl⟩

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

Goal state before:
pp: case neg
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsDiscreteValuationRing A
ϖ : A
hϖ : Irreducible ϖ
n : ℕ
u : Aˣ
hx : ¬↑u * ϖ ^ n = 0
⊢ (maximalIdeal A).intValuation (↑u * ϖ ^ n) = (ENat.recTopCoe 0 (fun x ↦ ↑(ofAdd ↑x)) ((addVal A) (↑u * ϖ ^ n)))⁻¹

Tactic:
have : (maximalIdeal A).intValuation ↑u = 1 := by simp [maximalIdeal]

Goal state after:
case neg
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsDiscreteValuationRing A
ϖ : A
hϖ : Irreducible ϖ
n : ℕ
u : Aˣ
hx : ¬↑u * ϖ ^ n = 0
this : (maximalIdeal A).intValuation ↑u = 1
⊢ (maximalIdeal A).intValuation (↑u * ϖ ^ n) = (ENat.recTopCoe 0 (fun x ↦ ↑(ofAdd ↑x)) ((addVal A) (↑u * ϖ ^ n)))⁻¹
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: 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
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : closure {x} = closure {x'}
hyc : closure {y} = closure {y'}
⊢ ∀ (a : G) (b : a ∈ closure {x}), ⟨a, b⟩ ∈ zpowers ⟨x', ⋯⟩

Tactic:
hxc,

Goal state after:
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
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : closure {x} = closure {x'}
hyc : closure {y} = closure {y'}
⊢ ∀ (a : G) (b : a ∈ closure {x'}), ⟨a, ⋯⟩ ∈ zpowers ⟨x', ⋯⟩
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mpr
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
⊢ Nonempty (G ≃+o ℤ) → {x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2

Tactic:
rintro ⟨f⟩

Goal state after:
case mpr
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
f : G ≃+o ℤ
⊢ {x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: 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
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a = 0
⊢ False

Tactic:
simp only [ha₀, map_zero] at ha

Goal state after:
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
hlmax_ge_1 : lmax ≥ 1
a : K
ha₀ : a = 0
ha : 0 = lmax
⊢ False
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → (coeff (d, n).1) p * (coeff (d, n).2) (X ^ n) = 0

Tactic:
exact fun h1 => (h1 (mem_antidiagonal.2 rfl)).elim

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

Goal state before:
pp: case h₀.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + (i, j).1)
h2 : (i, j) ≠ ((i, j).1, d)
⊢ (i, j) = ((i, j).1, d)

Tactic:
rw [mem_antidiagonal, add_comm, add_right_cancel_iff] at h1

Goal state after:
case h₀.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j).2 = d
h2 : (i, j) ≠ ((i, j).1, d)
⊢ (i, j) = ((i, j).1, d)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (n, d) ∉ antidiagonal (n + d) → (coeff (n, d).1) (X ^ n) * (coeff (n, d).2) p = 0

Tactic:
exact fun h1 => (h1 (mem_antidiagonal.2 rfl)).elim

Goal state after: