mathlib-initiative/mathlib-tactics huggingface dataset:
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✝³ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a b : D.obj i ⟶ X
ha : t.app i = a ≫ f
hb : t.app i = b ≫ f
hab : c.π.app i ≫ a = c.π.app i ≫ b
this✝ : ∀ (i : I), IsAffineHom (c.π.app i)
A : ExistsHomHomCompEqCompAux D t f :=
  { c := c, hc := hc, i := i, a := a, ha := ha, b := b, hb := hb, hab := hab, 𝒰S := S.affineCover, h𝒰S := ⋯,
    𝒰X := fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i).affineCover, h𝒰X := ⋯ }
𝒰 : (pullback.diagonalObj f).OpenCover := Pullback.diagonalCover f A.𝒰S A.𝒰X
W : (pullback.diagonalObj f).Opens := Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
k : A.𝒰D.I₀ → I
hki' : (j : A.𝒰D.I₀) → k j ⟶ A.i'
heq :
  ∀ (j : A.𝒰D.I₀),
    (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.a =
      (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.b
𝒰Df : (D.obj A.i').OpenCover := A.𝒰D.finiteSubcover
h : Nonempty ↥(D.obj A.i')
O : Finset I := {A.i'} ∪ Finset.image (fun i ↦ k (Cover.idx A.𝒰D ↑i)) Finset.univ
o : 𝒰Df.I₀ := ⋯.some
ho : k (Cover.idx A.𝒰D ↑o) ∈ O
l : I
hl1 : {X : I} → X ∈ O → (l ⟶ X)
hl2 :
  ∀ {X_1 Y : I} (mX : X_1 ∈ O) (mY : Y ∈ O) {f_1 : X_1 ⟶ Y},
    ⟨X_1, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈
        Finset.image (fun i ↦ ⟨k (Cover.idx A.𝒰D ↑i), ⟨A.i', ⟨⋯, ⟨⋯, hki' (Cover.idx A.𝒰D ↑i)⟩⟩⟩⟩) Finset.univ →
      hl1 mX ≫ f_1 = hl1 mY
this : ∀ (w v : 𝒰Df.I₀), hl1 ⋯ ≫ hki' (Cover.idx A.𝒰D ↑w) = hl1 ⋯ ≫ hki' (Cover.idx A.𝒰D ↑v)
u : (Precoverage.ZeroHypercover.pullback₁ (D.map (hl1 ho ≫ hki' (Cover.idx A.𝒰D ↑o))) 𝒰Df).I₀
F : pullback (D.map (hl1 ho ≫ hki' (Cover.idx A.𝒰D ↑o))) (𝒰Df.f u) ⟶
  pullback (D.map (hki' (Cover.idx A.𝒰D ↑u))) (A.𝒰D.f (Cover.idx A.𝒰D ↑u)) :=
  pullback.map (D.map (hl1 ho ≫ hki' (Cover.idx A.𝒰D ↑o))) (𝒰Df.f u) (D.map (hki' (Cover.idx A.𝒰D ↑u)))
    (A.𝒰D.f (Cover.idx A.𝒰D ↑u)) (D.map (hl1 ⋯)) (𝟙 (𝒰Df.X u)) (𝟙 (D.obj A.i')) ⋯ ⋯
⊢ k (Cover.idx A.𝒰D ↑u) ∈ O

Tactic:
by simp [O]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.c₆ = -W.b₂ ^ 3

Tactic:
rw [c₆]
  linear_combination (12 * W.b₂ * W.b₄ - 72 * W.b₆) * CharP.cast_eq_zero R 3

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case e'_2
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)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
x : ↥(D.obj i)
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : x ∈ ↑U
this : ∀ (j : Over i), IsAffine ((opensDiagram D i U).obj j)
j : Over i
f : j ⟶ Over.mk (𝟙 i)
hj :
  (ConcreteCategory.hom (Scheme.Hom.appTop ((opensDiagram D i U).map f)))
      ((ConcreteCategory.hom (Scheme.Hom.appTop ((opensDiagramι D i U).app (Over.mk (𝟙 i))))) s) =
    0
hf : Over.Hom.left f = j.hom
t' : Γ(↑(D.map j.hom ⁻¹ᵁ U), ⊤) ⟶ Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ U) := (D.obj j.left).presheaf.map (eqToHom ⋯).op
⊢ (ConcreteCategory.hom (Scheme.Hom.app (D.map j.hom) U)) ((s |_ U) ⋯) =
    (ConcreteCategory.hom t')
      ((ConcreteCategory.hom (Scheme.Hom.appTop ((opensDiagram D i U).map f)))
        ((ConcreteCategory.hom (Scheme.Hom.appTop ((opensDiagramι D i U).app (Over.mk (𝟙 i))))) s))

Tactic:
dsimp [TopCat.Presheaf.restrictOpen, TopCat.Presheaf.restrict]
      simp only [Scheme.Hom.app_eq_appLE, homOfLE_leOfHom, ← ConcreteCategory.comp_apply, hf,
        Scheme.Hom.map_appLE, TopologicalSpace.Opens.map_top, Scheme.Hom.resLE_appLE]
      simp [t']

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y W'.negPolynomial = W'.negY x y

Tactic:
rw [negY, sub_sub, negPolynomial]
  eval_simp

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst✝ : W.IsElliptic
⊢ ↑(C • W).Δ' = ↑C.u⁻¹ ^ 12 * ↑W.Δ'

Tactic:
by
  simp_rw [coe_Δ', variableChange_Δ]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case refine_3
R : Type u_2
inst✝ : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf : ∀ (i : Fin n), (f (MvPolynomial.X i)).degrees ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
hg : g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) = ↑f
σ : MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) (MvPolynomial (Fin n) R) :=
  MvPolynomial.map (algebraMap R (MvPolynomial (Fin n) R))
hσ : g.comp σ = RingHom.id (MvPolynomial (Fin m) R)
hσ' : ∀ (x : MvPolynomial (Fin m) R), g (σ x) = x
hg' : Surjective ⇑g
S' : ConstructibleSetData (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Finset.image
    (fun x ↦
      match x with
      | { f := fk, n := k, g := gk } =>
        { f := σ fk, n := k + n,
          g := fun s ↦
            Sum.elim (⇑σ ∘ gk) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i)))
              (finSumFinEquiv.symm s) })
    S
s₀ : Set (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Set.range fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))
hs : zeroLocus s₀ = Set.range (comap g)
t : Set (PrimeSpectrum (MvPolynomial (Fin m) R))
⊢ comap g ⁻¹' comap g '' t = comap g ⁻¹' (comap σ ⁻¹' t ∩ zeroLocus s₀)

Tactic:
· rw [Set.preimage_image_eq _ (comap_injective_of_surjective g hg'),
        Set.preimage_inter, hs, Set.preimage_range, Set.inter_univ,
        ← Set.preimage_comp, ← comap_comp, hσ]
      simp only [comap_id, Set.preimage_id']

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
m : ℕ
⊢ -preNormEDS b c d (2 * ↑m + 1) =
    (-preNormEDS b c d (↑m - 1) * (-preNormEDS b c d (↑m + 1)) ^ 3 * if Even (-(↑m + 1)) then b else 1) -
      -preNormEDS b c d (↑m + 2) * (-preNormEDS b c d ↑m) ^ 3 * if Even (-(↑m + 1)) then 1 else b

Tactic:
even_neg,

Goal state after:
case neg.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
m : ℕ
⊢ -preNormEDS b c d (2 * ↑m + 1) =
    (-preNormEDS b c d (↑m - 1) * (-preNormEDS b c d (↑m + 1)) ^ 3 * if Even (↑m + 1) then b else 1) -
      -preNormEDS b c d (↑m + 2) * (-preNormEDS b c d ↑m) ^ 3 * if Even (↑m + 1) then 1 else b
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
n : ℤ
⊢ (-preNormEDS (b ^ 4) c d n * if Even (-n) then b else 1) = -(preNormEDS (b ^ 4) c d n * if Even n then b else 1)

Tactic:
even_neg,

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
n : ℤ
⊢ (-preNormEDS (b ^ 4) c d n * if Even n then b else 1) = -(preNormEDS (b ^ 4) c d n * if Even n then b else 1)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ (preNormEDS (b ^ 4) c d (2 * k) * if Even k then b else b) =
    preNormEDS (b ^ 4) c d (2 * k) * if Even (2 * k) then b else 1

Tactic:
ite_self,

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ preNormEDS (b ^ 4) c d (2 * k) * b = preNormEDS (b ^ 4) c d (2 * k) * if Even (2 * k) then b else 1
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
by
  induction m using Int.negInduction with
  | nat m =>
    rcases m with _ | _
    · simp
    norm_cast
    simpa only [complEDS_ofNat] using! complEDS'_even ..
  | neg ih => simp_rw [mul_neg, complEDS_neg, ih, neg_mul, complEDS₂_neg]

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

Goal state before:
pp: case pos
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
hp : ¬p = 0
hq : q = 0
⊢ 2 • p.degree = max (2 • p.degree) (2 • degree 0 + 3)

Tactic:
exact (max_bot_right _).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_3.refine_5
I : Type u
inst✝⁶ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁵ : IsCofiltered I
inst✝⁴ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝³ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝² : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
𝒰 : c.pt.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : Finite 𝒰.I₀
i : I
V : 𝒰.I₀ → (D.obj i).Opens
hV : TopologicalSpace.IsOpenCover V
hV' : ∀ (j : 𝒰.I₀), IsAffineOpen (V j) ∧ Hom.opensRange (𝒰.f j) = c.π.app i ⁻¹ᵁ V j
hV'' : ∀ (k : 𝒰.I₀), Set.range ⇑(𝒰.f k) = ⇑(c.π.app i) ⁻¹' ↑(V k)
k : 𝒰.I₀
⊢ ∀ (s : PullbackCone ⋯.fromSpec (c.π.app i)) (m : s.pt ⟶ 𝒰.X k),
    m ≫ IsOpenImmersion.lift (V k).ι (𝒰.f k ≫ c.π.app i) ⋯ ≫ ⋯.isoSpec.hom = s.fst →
      m ≫ 𝒰.f k = s.snd → m = IsOpenImmersion.lift (𝒰.f k) s.snd ⋯

Tactic:
simp [← cancel_mono (𝒰.f k)]

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
f : R →+* S
n : ℕ
⊢ (W.map f).preΨ' n = Polynomial.map f (W.preΨ' n)

Tactic:
simp [preΨ', ← coe_mapRingHom]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ W.c₄ = 0

Tactic:
rw [c₄_of_isShortNF]

Goal state after:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ -48 * W.a₄ = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve R
inst✝¹ : CharP R 3
inst✝ : CharP F 3
⊢ 2 * 2 = 1

Tactic:
by linear_combination CharP.cast_eq_zero R 3

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < n
h : ↑n ≠ 0
⊢ 2 ≤ n ^ 2 - if Even n then 4 else 1

Tactic:
split_ifs <;> exact Nat.AtLeastTwo.prop.trans <| Nat.sub_le_sub_right (Nat.pow_le_pow_left hn 2) _

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 : ℕ), (W.preΨ ↑n).natDegree ≤ ((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2
n✝ : ℕ
⊢ (W.preΨ ↑n✝).natDegree ≤ ((↑n✝).natAbs ^ 2 - if Even (-↑n✝) then 4 else 1) / 2

Tactic:
even_neg,

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.preΨ ↑n).natDegree ≤ ((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2
n✝ : ℕ
⊢ (W.preΨ ↑n✝).natDegree ≤ ((↑n✝).natAbs ^ 2 - if Even ↑n✝ then 4 else 1) / 2
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
heq : E.j = E'.j
p : ℕ
h✝ : CharP F p
hchar2 : ¬p = 2
hchar3 : ¬p = 3
⊢ ∃ C, C • E = E'

Tactic:
exact exists_variableChange_of_char_ne_two_or_three _ _ hchar2 hchar3 heq

Goal state after:
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
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.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) = -W.dblU P / W.dblZ P

Tactic:
simp only [X_eq_iff hPz hQz, ne_eq, Y_eq_iff' hPz hQz] at hx hy

Goal state after:
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x / P z ^ 2 = Q x / Q z ^ 2
hy : ¬P y / P z ^ 3 = W.toAffine.negY (Q x / Q z ^ 2) (Q y / Q 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.dblU P / W.dblZ P
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
⊢ (if hx : x * y = 0 then 0 else e ^ toAdd (unzero hx)) =
    (if hx : x = 0 then 0 else e ^ toAdd (unzero hx)) * if hx : y = 0 then 0 else e ^ toAdd (unzero hx)

Tactic:
by
    by_cases hxy : x * y = 0
    · rcases mul_eq_zero.mp hxy with hx | hy
      -- either x = 0 or y = 0
      · rw [dif_pos hxy, dif_pos hx, zero_mul]
      · rw [dif_pos hxy, dif_pos hy, mul_zero]
    · obtain ⟨hx, hy⟩ := mul_ne_zero_iff.mp hxy
      -- x ≠ 0 and y ≠ 0
      rw [dif_neg hxy, dif_neg hx, dif_neg hy, ← zpow_add' (Or.inl he), ← toAdd_mul]
      congr
      rw [← WithZero.coe_inj, WithZero.coe_mul, coe_unzero hx, coe_unzero hy, coe_unzero hxy]

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : NonarchimedeanRing R
U : OpenAddSubgroup R
⊢ ∃ V, ↑V * ↑V ⊆ ↑U

Tactic:
let ⟨V, H⟩ := prod_self_subset <| (U.isOpen.preimage continuous_mul).mem_nhds <| by
    simpa only [Set.mem_preimage, Prod.snd_zero, mul_zero] using! U.zero_mem
  use V
  rintro v ⟨a, ha, b, hb, hv⟩
  have hy := H (Set.mk_mem_prod ha hb)
  simp only [Set.mem_preimage, SetLike.mem_coe, hv] at hy
  rw [SetLike.mem_coe]
  exact hy

Goal state after:
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
hZ : ∀ {n : ℕ}, IsUnit (W.dblZ P ^ n)
⊢ ![W.dblX P, W.dblY P, W.dblZ P] =
    ![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)),
            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]
          x,
      W.dblZ P ^ 3 *
        ![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]
          y,
      W.dblZ P *
        ![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]
          z]

Tactic:
← dblX_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
hZ : ∀ {n : ℕ}, IsUnit (W.dblZ P ^ n)
⊢ ![W.dblX P, W.dblY P, W.dblZ P] =
    ![W.dblZ P ^ 2 *
        ![W.dblX P / W.dblZ P ^ 2,
            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]
          x,
      W.dblZ P ^ 3 *
        ![W.dblX P / W.dblZ P ^ 2,
            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]
          y,
      W.dblZ P *
        ![W.dblX P / W.dblZ P ^ 2,
            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]
          z]
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case mk.mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z x✝² : R
y✝² : ↥(posSubmonoid R)
x✝¹ : R
y✝¹ : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk x✝² y✝² ≤ ValueGroupWithZero.mk x✝¹ y✝¹
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ x✝² * ↑y✝¹ * (x✝ * ↑y✝) ≤ᵥ x✝¹ * ↑y✝² * (x✝ * ↑y✝)

Tactic:
exact mul_vle_mul_left hab _

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

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.negAddY P Q + (W'.negY Q - Q y) * Q z ^ 3 * P x ^ 3 -
      ((P x * Q z) ^ 3 * W'.negY Q + (W'.negY Q - Q y) * Q z ^ 3 * P y ^ 2) =
    0

Tactic:
rw [negAddY, negY, hPz]; ring1

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x y v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I ↑(span {v * x}) = span {y}
z : R
hi : z * y * x ∈ I
⊢ z * (x * y) = z * y * x

Tactic:
rw [mul_assoc, mul_comm y]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ ![(P x * Q z) ^ 2 * Q x, W'.addY P Q, addZ P Q] = (P x * Q z) • Q

Tactic:
addY_of_Z_eq_zero_left hP hPz,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ ![(P x * Q z) ^ 2 * Q x, (P x * Q z) ^ 3 * Q y, addZ P Q] = (P x * Q z) • Q
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : G ≃*o WithZero (Multiplicative ℤ)
a✝ b✝ : Gˣ
⊢ unzero ⋯ ≤ unzero ⋯ ↔ f ↑a✝ ≤ f ↑b✝

Tactic:
← coe_le_coe,

Goal state after:
case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : G ≃*o WithZero (Multiplicative ℤ)
a✝ b✝ : Gˣ
⊢ ↑(unzero ⋯) ≤ ↑(unzero ⋯) ↔ f ↑a✝ ≤ f ↑b✝
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
⊢ Nonempty (G ≃*o WithZero (Multiplicative ℤ)) ↔ ¬DenselyOrdered G

Tactic:
rw [← denselyOrdered_units_iff,
      ← LinearOrderedCommGroup.discrete_iff_not_denselyOrdered]
  refine Nonempty.congr ?_ ?_ <;> intro f
  · refine ⟨MulEquiv.withZero.symm (withZeroUnitsEquiv.trans f), ?_⟩
    intros
    simp only [MulEquiv.withZero, withZeroUnitsEquiv, MulEquiv.trans_apply,
      MulEquiv.coe_mk, Equiv.coe_fn_mk, recZeroCoe_coe, OrderMonoidIso.coe_mulEquiv,
      MulEquiv.symm_trans_apply, MulEquiv.symm_mk, Equiv.coe_fn_symm_mk, map_eq_zero, coe_ne_zero,
      ↓reduceDIte, unzero_coe, MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe]
    rw [← Units.val_le_val, ← map_le_map_iff f, ← coe_le_coe, coe_unzero, coe_unzero]
  · refine ⟨withZeroUnitsEquiv.symm.trans (MulEquiv.withZero f), ?_⟩
    intros
    simp only [withZeroUnitsEquiv, MulEquiv.symm_mk, MulEquiv.withZero,
      MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe,
      MulEquiv.trans_apply, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk]
    split_ifs <;>
    simp_all [← Units.val_le_val]

Goal state after:
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₀
⊢ ∃ C, IsIntegral R (C • W)

Tactic:
let lmax : ValueGroup R K :=
    l.maximum_of_length_pos (by simp [l₀, l])

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 ⋯
⊢ ∃ C, IsIntegral R (C • W)
Module: Mathlib.GroupTheory.ArchimedeanDensely

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

Tactic:
by
  rw [← wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete (g := -g)]
  refine ⟨fun h ↦ (h.mapsTo (- ·) ?_).mono' ?_, fun h ↦ (h.mapsTo (- ·) ?_).mono' ?_⟩ <;>
  · intro
    simp [Function.onFun, neg_le]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
m n : σ →₀ ℕ
a : R
⊢ (LinearMap.proj m) ((monomial n) a) = if m = n then a else 0

Tactic:
rw [monomial_def, LinearMap.proj_apply (i := m), LinearMap.single_apply, Pi.single_apply]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : n ≤ d
⊢ (coeff d) (p * X ^ n) = (coeff (d - n)) p

pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
⊢ (coeff d) (p * X ^ n) = 0

Tactic:
· rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
⊢ (coeff d) (p * X ^ n) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff n) (φ * ψ) = (coeff n) (ψ * φ)

Tactic:
classical
      simpa only [coeff_mul, mul_comm] using
        sum_antidiagonal_swap n fun a b => coeff a φ * coeff b ψ

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
⊢ v.intValuation r = exp (-↑(multiplicity v.asIdeal (Ideal.span {r})))

Tactic:
have hsr : Ideal.span {r} ≠ 0 := Submodule.span_singleton_eq_bot.mp.mt hr
  have hfm : FiniteMultiplicity v.asIdeal (Ideal.span {r}) :=
    FiniteMultiplicity.of_prime_left v.prime hsr
  rw [v.intValuation_if_neg hr, exp_inj, neg_inj, Int.natCast_inj, ← ENat.natCast_inj,
    ← FiniteMultiplicity.emultiplicity_eq_multiplicity hfm,
    UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors (irreducible v) hsr,
    normalize_eq, Ideal.count_associates_factors_eq hsr v.isPrime v.ne_bot]

Goal state after: