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.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ W.Δ = W.a₆

Tactic:
Δ,

Goal state after:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ -W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆ = W.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ W.Δ = -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)

Tactic:
Δ,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ -W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆ = -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)
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
⊢ ∃ k fk,
    ∀ (j : ↥s),
      ∃ ak,
        ak ≫ f = (D.map fk ⁻¹ᵁ 𝒱 j).ι ≫ t.app k ∧
          c.π.app k ∣_ D.map fk ⁻¹ᵁ 𝒱 j ≫ ak = (c.π.app k ⁻¹ᵁ D.map fk ⁻¹ᵁ 𝒱 j).ι ≫ a

Tactic:
have _ (j k) : IsAffine ((opensDiagram D i' (𝒱' j)).obj k) := ((h𝒱𝒰 _).1.preimage _).preimage _

Goal state after:
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)
⊢ ∃ k fk,
    ∀ (j : ↥s),
      ∃ ak,
        ak ≫ f = (D.map fk ⁻¹ᵁ 𝒱 j).ι ≫ t.app k ∧
          c.π.app k ∣_ D.map fk ⁻¹ᵁ 𝒱 j ≫ ak = (c.π.app k ⁻¹ᵁ D.map fk ⁻¹ᵁ 𝒱 j).ι ≫ a
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] = P

Tactic:
ext n; fin_cases n <;> rfl

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

Goal state before:
pp: case e'_3
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ ↑(if Even n then n / 2 else n) = ↑(expCoeff n)

Tactic:
rcases n.even_or_odd' with ⟨n, rfl | rfl⟩

Goal state after:
case e'_3.inl
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ ↑(if Even (2 * n) then 2 * n / 2 else 2 * n) = ↑(expCoeff (2 * n))

case e'_3.inr
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ ↑(if Even (2 * n + 1) then (2 * n + 1) / 2 else 2 * n + 1) = ↑(expCoeff (2 * n + 1))
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
  rcases n.even_or_odd' with ⟨n, rfl | rfl⟩ <;> simp [expCoeff, n.not_even_two_mul_add_one]

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 ^ 2 - if Even n then 4 else 1) / 2) ≠ 0

Tactic:
rcases n.even_or_odd' with ⟨n, rfl | rfl⟩

Goal state after:
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

case inr
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑(2 * n + 1) ≠ 0
⊢ (W.preΨ' (2 * n + 1)).coeff (((2 * n + 1) ^ 2 - if Even (2 * n + 1) then 4 else 1) / 2) ≠ 0
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.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 ≠ Q y * P z ^ 3
⊢ W.add P Q = addU P Q • ![1, 1, 0]

Tactic:
add_of_not_equiv <| not_equiv_of_Y_ne hy,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian 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 ≠ Q y * P z ^ 3
⊢ W.addXYZ P Q = addU P Q • ![1, 1, 0]
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.dblY P / W.dblZ P ^ 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:
erw [dblY, negY_of_Z_ne_zero <| dblZ_ne_zero_of_Y_ne' hP hQ hPz hx hy,
    dblX_of_Z_ne_zero hP hQ hPz hQz hx hy, negDblY_of_Z_ne_zero hP hQ hPz hQz hx hy, Affine.addY]

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 Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
this :
  W.Nonsingular
    ![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.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)),
      1]
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.Nonsingular (W.add P Q)

pp: case neg
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
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
this :
  W.Nonsingular
    ![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.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)),
      1]
hx : ¬P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.Nonsingular (W.add P Q)

Tactic:
· simpa only [add_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx,
            nonsingular_smul _ <| isUnit_dblZ_of_Y_ne' hP.left hQ.left hPz hx <| not_and.mp hxy hx]

Goal state after:
case neg
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
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
this :
  W.Nonsingular
    ![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.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)),
      1]
hx : ¬P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.Nonsingular (W.add P Q)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift ⟦Q⟧
hQz : ¬Q z = 0
⊢ ⟦(P x * Q z) • Q⟧ = ⟦Q⟧

Tactic:
smul_eq _ <| (isUnit_X_of_Z_eq_zero hP hPz).mul <| Ne.isUnit hQz

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift ⟦Q⟧
hQz : ¬Q z = 0
⊢ ⟦Q⟧ = ⟦Q⟧
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.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.addMap ⟦P⟧ ⟦Q⟧ = ⟦![1, 1, 0]⟧

Tactic:
by_cases hy : P y * Q z ^ 3 = Q y * P z ^ 3
  · rw [addMap_eq, add_of_Y_eq hPz hQz hx hy hy',
      smul_eq _ <| isUnit_dblU_of_Y_eq hP hPz hQz hx hy hy']
  · rw [addMap_eq, add_of_Y_ne hP.left hQ hPz hQz hx hy,
      smul_eq _ <| isUnit_addU_of_Y_ne hPz hQz hy]

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

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
⊢ Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Tactic:
by
  let := B.uniformSpace
  have := B.isUniformAddGroup
  suffices F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ᵉ (x ∈ M) (y ∈ M), y - x ∈ U by
    constructor <;> rintro ⟨h', h⟩ <;> refine ⟨h', ?_⟩ <;> [rwa [← this]; rwa [this]]
  rw [uniformity_eq_comap_nhds_zero G, ← map_le_iff_le_comap]
  change Tendsto _ _ _ ↔ _
  simp [(basis_sets F).prod_self.tendsto_iff B.nhds_zero_hasBasis, @forall_comm (_ ∈ _) G]

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₀ˣ
Hx : v x = 0
y : R
a✝ : y ∈ ↑(v.ltAddSubgroup ((Units.map ↑embedding) 1))
⊢ v (x * y) < ↑((Units.map ↑embedding) γ)

Tactic:
rw [Valuation.map_mul, Hx, zero_mul]

Goal state after:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
Hx : v x = 0
y : R
a✝ : y ∈ ↑(v.ltAddSubgroup ((Units.map ↑embedding) 1))
⊢ 0 < ↑((Units.map ↑embedding) γ)
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: 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) ⋯
⊢ embedding ↑u⁻¹ = ↑γx⁻¹

Tactic:
simp [restrict₀_apply, embedding_apply, hu_def, Hx]

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

Goal state before:
pp: case neg
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:
by_cases hQz : Q z = 0
    · rw [add_of_Z_eq_zero_right hQ.left hPz hQz,
        toAffine_smul _ ((isUnit_X_of_Z_eq_zero hQ hQz).mul <| Ne.isUnit hPz).neg,
        toAffine_of_Z_eq_zero hQz, add_zero]
    · by_cases hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
      · rw [toAffine_of_Z_ne_zero hP hPz, toAffine_of_Z_ne_zero hQ hQz, Affine.Point.add_of_Y_eq
            ((X_eq_iff hPz hQz).mp hxy.left) ((Y_eq_iff' hPz hQz).mp hxy.right)]
        by_cases hy : P y * Q z ^ 3 = Q y * P z ^ 3
        · rw [add_of_Y_eq hPz hQz hxy.left hy hxy.right,
            toAffine_smul _ <| isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, toAffine_zero]
        · rw [add_of_Y_ne hP.left hQ.left hPz hQz hxy.left hy,
            toAffine_smul _ <| isUnit_addU_of_Y_ne hPz hQz hy, toAffine_zero]
      · have := toAffine_add_of_Z_ne_zero hP hQ hPz hQz hxy
        by_cases hx : P x * Q z ^ 2 = Q x * P z ^ 2
        · rwa [add_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx,
            toAffine_smul _ <| isUnit_dblZ_of_Y_ne' hP.left hQ.left hPz hx <| not_and.mp hxy hx]
        · rwa [add_of_X_ne hP.left hQ.left hPz hQz hx, toAffine_smul _ <| isUnit_addZ_of_X_ne hx]

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

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Jacobian R
W : Jacobian F
inst✝ : DecidableEq F
⊢ Function.LeftInverse fromAffine toAffineLift

Tactic:
rintro @⟨⟨P⟩, hP⟩
    by_cases hPz : P z = 0
    · rw [Point.ext_iff, toAffineLift_eq, toAffine_of_Z_eq_zero hPz]
      exact Quotient.eq.mpr <| Setoid.symm <| equiv_zero_of_Z_eq_zero hP hPz
    · rw [Point.ext_iff, toAffineLift_eq, toAffine_of_Z_ne_zero hP hPz]
      exact Quotient.eq.mpr <| Setoid.symm <| equiv_some_of_Z_ne_zero hPz

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : R
s : ↥(posSubmonoid R)
⊢ 0 < ValueGroupWithZero.mk x s ↔ 0 <ᵥ x

Tactic:
← mk_zero 1

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : R
s : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk 0 1 < ValueGroupWithZero.mk x s ↔ 0 <ᵥ x
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
⊢ v ↑π.val ^ m ≤ 1

Tactic:
hm'

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
⊢ v ↑r ≤ 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Jacobian R
f : R →+* S
P Q : Fin 3 → R
⊢ (W'.map f).addX (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addX P Q)

Tactic:
by
  simp only [addX]
  map_simp

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

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (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
⊢ Valued.v.restrict ((equiv v) r) / Valued.v.restrict ((equiv v) s) ≠ 0

Tactic:
simp only [equiv_apply, restrict_def, ne_eq, div_eq_zero_iff, restrict₀_eq_zero_iff, hv,
      MonoidWithZeroHom.coe_ofClass, not_or, (eq_zero h (r := r.ofVal)).ne,
      (eq_zero h (r := s.ofVal)).ne]
    exact ⟨hr₀.ne', hs₀.ne'⟩

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

Goal state before:
pp: case h
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
x_ne : x ≠ 0
s : Set K
γ : (ofClass v).ValueGroup₀ˣ
hs : {y | v.restrict (y - x⁻¹) < ↑γ} ⊆ s
γ' : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
y : K
y_in : v.restrict (y - x) < min (↑γ * (↑γ' * ↑γ')) ↑γ'
⊢ y⁻¹ ∈ {y | v.restrict (y - x⁻¹) < ↑γ}

Tactic:
exact Valuation.inversion_estimate _ x_ne y_in

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ha : a ≠ 1
this : Function.Injective fun x ↦ a ^ x
⊢ (∃ n, a ^ n = b) → ∃! k, a ^ k = b

Tactic:
rintro ⟨m, rfl⟩
      exact ⟨m, rfl, fun k hk ↦ this hk⟩

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G✝ : Type u_1
inst✝⁷ : CommGroup G✝
inst✝⁶ : LinearOrder G✝
inst✝⁵ : IsOrderedMonoid G✝
inst✝⁴ : MulArchimedean G✝
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x : G
h : IsLeast {y | 0 < y} x
this : ⊤ = AddSubgroup.closure {x}
⊢ G ≃+o ℤ

Tactic:
let e : G ≃+o (⊤ : AddSubgroup G) := ⟨AddSubsemigroup.topEquiv.symm,
    (AddEquiv.strictMono_symm AddSubsemigroup.strictMono_topEquiv).le_iff_le⟩

Goal state after:
G✝ : Type u_1
inst✝⁷ : CommGroup G✝
inst✝⁶ : LinearOrder G✝
inst✝⁵ : IsOrderedMonoid G✝
inst✝⁴ : MulArchimedean G✝
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x : G
h : IsLeast {y | 0 < y} x
this : ⊤ = AddSubgroup.closure {x}
e : G ≃+o ↥⊤ := { toAddEquiv := AddSubsemigroup.topEquiv.symm, map_le_map_iff' := ⋯ }
⊢ G ≃+o ℤ
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
W : WeierstrassCurve K
inst✝ : IsIntegral R W
W_int : WeierstrassCurve R
hW_int : W = W_int⁄K
⊢ (algebraMap R K) W_int.Δ = (W_int⁄K).Δ

Tactic:
baseChange,

Goal state after:
case h
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
W : WeierstrassCurve K
inst✝ : IsIntegral R W
W_int : WeierstrassCurve R
hW_int : W = W_int⁄K
⊢ (algebraMap R K) W_int.Δ = (W_int.map (algebraMap R K)).Δ
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
hx : (restrict₀ (ofClass v)) ⋯.choose = a
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : (restrict₀ (ofClass v)) ⋯.choose = b
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
⊢ extensionValuation.restrict ↑xy = extensionValuation.restrict ↑x * extensionValuation.restrict ↑y

Tactic:
have hxy := (restrict₀_surjective (.ofClass hv.v) (a * b)).choose_spec

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
hx : (restrict₀ (ofClass v)) ⋯.choose = a
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : (restrict₀ (ofClass v)) ⋯.choose = b
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
hxy : (restrict₀ (ofClass v)) ⋯.choose = a * b
⊢ extensionValuation.restrict ↑xy = extensionValuation.restrict ↑x * extensionValuation.restrict ↑y
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
⊢ ∑ p ∈ antidiagonal (single () n), (MvPowerSeries.coeff p.1) φ * (MvPowerSeries.coeff p.2) ψ =
    ∑ p ∈ antidiagonal n, (coeff p.1) φ * (coeff p.2) ψ

Tactic:
Finsupp.antidiagonal_single,

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
⊢ ∑ p ∈ Finset.map ({ toFun := single (), inj' := ⋯ }.prodMap { toFun := single (), inj' := ⋯ }) (antidiagonal n),
      (MvPowerSeries.coeff p.1) φ * (MvPowerSeries.coeff p.2) ψ =
    ∑ p ∈ antidiagonal n, (coeff p.1) φ * (coeff p.2) ψ
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a : R
⊢ a • f = C a * f

Tactic:
by
  ext
  simp

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

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (m : σ →₀ ℕ), Commute ((coeff m) φ) a
m : σ →₀ ℕ
⊢ (if n ≤ m then (coeff (m - n)) φ * a else 0) = (coeff m) ((monomial n) a * φ)

Tactic:
coeff_monomial_mul

Goal state after:
case refine_2
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (m : σ →₀ ℕ), Commute ((coeff m) φ) a
m : σ →₀ ℕ
⊢ (if n ≤ m then (coeff (m - n)) φ * a else 0) = if n ≤ m then a * (coeff (m - n)) φ else 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
a : R
⊢ a • f = C a * f

Tactic:
by
  ext
  simp

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

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
hab : extensionValuation.restrict ↑⋯.choose = extensionValuation.restrict ↑⋯.choose
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ha0 : a = 0
⊢ embedding a = embedding b

Tactic:
have h0 : extension ((algebraMap K (hat K)) x) = 0 := by
        simpa [ha0, extension_eq_zero_iff, map_eq_zero] using hx

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
hab : extensionValuation.restrict ↑⋯.choose = extensionValuation.restrict ↑⋯.choose
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ha0 : a = 0
h0 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ embedding a = embedding b
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
i : ℕ
hi : i ∈ range n ∧ k i = 0
⊢ k i = 0

Tactic:
rw [hi.2]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R[X]
⊢ ↑(φ + ψ) = ↑φ + ↑ψ

Tactic:
by
  ext
  simp

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

Goal state before:
pp: U : Type u_2
V : Type u_3
inst✝¹ : CommSemiring U
inst✝ : CommSemiring V
φ : U →+* V
f : U[X]
⊢ ↑(map φ f) = (PowerSeries.map φ) ↑f

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ constantCoeff f = 0 → 1 ≤ f.order

Tactic:
· intro h
    refine MvPowerSeries.le_order fun d hd ↦ ?_
    rw [Nat.cast_lt_one] at hd
    simp [(degree_eq_zero_iff d).mp hd, h]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p < weightedOrder w f
d : σ →₀ ℕ
⊢ (coeff d) ((weightedHomogeneousComponent w p) f) = (coeff d) 0

Tactic:
rw [coeff_weightedHomogeneousComponent]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p < weightedOrder w f
d : σ →₀ ℕ
⊢ (if (weight w) d = p then (coeff d) f else 0) = (coeff d) 0