mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case neg
R : Type u_2
inst✝ : CommRing R
n✝ n : ℕ
IH :
  ∀ {M : Submodule ℤ R},
    1 ∈ M →
      ∀ (k : ℕ) (d : Multiset (Fin n)) (S : ConstructibleSetData (MvPolynomial (Fin n) R)),
        (∀ C ∈ S, C.n ≤ k) →
          (∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) d)) →
            ∃ T,
              comap MvPolynomial.C '' S.toSet = T.toSet ∧
                ∀ C ∈ T,
                  C.n ≤ numBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n ∧
                    ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n
M : Submodule ℤ R
hM : 1 ∈ M
k : ℕ
d : Multiset (Fin (n + 1))
S : ConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS :
  ∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin (n + 1)) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin (n + 1)) d)
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] (MvPolynomial (Fin n) R)[X] := MvPolynomial.finSuccEquiv R n
S' : ConstructibleSetData (MvPolynomial (Fin n) R)[X] := ConstructibleSetData.map e.toRingEquiv.toRingHom S
C : BasicConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hxS : C ∈ S
j : Fin { f := e C.f, n := C.n, g := ⇑e ∘ C.g }.n
hj : j ∈ Finset.univ
hgj : ¬C.g j = 0
⊢ (↑(degreeOf 0 (C.g j))).succ ≤ 1 + Multiset.count 0 d

Tactic:
WithBot.succ_natCast,

Goal state after:
case neg
R : Type u_2
inst✝ : CommRing R
n✝ n : ℕ
IH :
  ∀ {M : Submodule ℤ R},
    1 ∈ M →
      ∀ (k : ℕ) (d : Multiset (Fin n)) (S : ConstructibleSetData (MvPolynomial (Fin n) R)),
        (∀ C ∈ S, C.n ≤ k) →
          (∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) d)) →
            ∃ T,
              comap MvPolynomial.C '' S.toSet = T.toSet ∧
                ∀ C ∈ T,
                  C.n ≤ numBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n ∧
                    ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n
M : Submodule ℤ R
hM : 1 ∈ M
k : ℕ
d : Multiset (Fin (n + 1))
S : ConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS :
  ∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin (n + 1)) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin (n + 1)) d)
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] (MvPolynomial (Fin n) R)[X] := MvPolynomial.finSuccEquiv R n
S' : ConstructibleSetData (MvPolynomial (Fin n) R)[X] := ConstructibleSetData.map e.toRingEquiv.toRingHom S
C : BasicConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hxS : C ∈ S
j : Fin { f := e C.f, n := C.n, g := ⇑e ∘ C.g }.n
hj : j ∈ Finset.univ
hgj : ¬C.g j = 0
⊢ ↑(degreeOf 0 (C.g j)) + 1 ≤ 1 + Multiset.count 0 d
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ W.slope x₁ x₂ y₁ y₂ = -evalEval x₁ y₁ W.polynomialX / evalEval x₁ y₁ W.polynomialY

Tactic:
rw [slope_of_Y_ne hx hy, evalEval_polynomialX, neg_sub]
  congr 1
  rw [negY, evalEval_polynomialY]
  ring1

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x : R
⊢ (C (X - C x)).natDegree < W'.polynomial.natDegree

Tactic:
rw [natDegree_polynomial, natDegree_C]

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x : R
⊢ 0 < 2
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case e'_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))
⊢ Ideal.span s₀ = RingHom.ker g

Tactic:
have H : Ideal.span s₀ ≤ RingHom.ker g := by
      simp only [Ideal.span_le, Set.range_subset_iff, SetLike.mem_coe, RingHom.mem_ker, map_sub,
        hσ', s₀]
      simp [g]

Goal state after:
case e'_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))
H : Ideal.span s₀ ≤ RingHom.ker g
⊢ Ideal.span s₀ = RingHom.ker g
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x₁ y₁ x₂ ℓ : R
⊢ (W'.map f).negAddY (f x₁) (f x₂) (f y₁) (f ℓ) = f (W'.negAddY x₁ x₂ y₁ ℓ)

Tactic:
simp only [negAddY, map_addX]
  map_simp

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atom W a b * atom W c d = atom W b a * atom W d c

Tactic:
by
  rw [← neg_atom odd a b, ← neg_atom odd c d, neg_mul_neg]

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) = rel W (a - d) (b - d) (c - d) (2 * d)

Tactic:
by
  simp_rw [rel_eq, mul_sub, sub_add_cancel]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case intro.refine_1
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)
J : Type u_1
inst✝ : Finite J
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
j : J → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
val✝ : Fintype J
i : I
fi : (k : J) → i ⟶ j k
k : I
fkj : k ⟶ i
e : D.map fkj ⁻¹ᵁ ⨆ k, D.map (fi k) ⁻¹ᵁ V k = ⊤
⊢ IsOpenCover fun x ↦ D.map (fkj ≫ fi x) ⁻¹ᵁ V x

Tactic:
refine top_le_iff.mp (e.symm.trans_le ?_)

Goal state after:
case intro.refine_1
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)
J : Type u_1
inst✝ : Finite J
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
j : J → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
val✝ : Fintype J
i : I
fi : (k : J) → i ⟶ j k
k : I
fkj : k ⟶ i
e : D.map fkj ⁻¹ᵁ ⨆ k, D.map (fi k) ⁻¹ᵁ V k = ⊤
⊢ D.map fkj ⁻¹ᵁ ⨆ k, D.map (fi k) ⁻¹ᵁ V k ≤ ⨆ x, D.map (fkj ≫ fi x) ⁻¹ᵁ V x
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case neg
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
⊢ (p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree =
    max (2 • p.degree) (2 • q.degree + 3)

Tactic:
rw [← not_congr degree_eq_bot] at hp hq
      -- Porting note: BUG `cases` tactic does not modify assumptions in `hp'` and `hq'`
      rcases hp' : p.degree with _ | dp -- `hp' : ` should be redundant
      · exact (hp hp').elim -- `hp'` should be `rfl`
      · rw [hp'] at hdp hdpq -- line should be redundant
        rcases hq' : q.degree with _ | dq -- `hq' : ` should be redundant
        · exact (hq hq').elim -- `hq'` should be `rfl`
        · rw [hq'] at hdpq hdq -- line should be redundant
          rcases le_or_gt dp (dq + 1) with hpq | hpq
          · convert!
            (degree_sub_eq_right_of_degree_lt <|
                  (degree_sub_le _ _).trans_lt <|
                    max_lt_iff.mpr ⟨hdp.trans_lt _, hdpq.trans_lt _⟩).trans
              (max_eq_right_of_lt _).symm <;> rw [hdq] <;>
                exact WithBot.coe_lt_coe.mpr <| by dsimp; linarith only [hpq]
          · rw [sub_sub]
            convert!
              (degree_sub_eq_left_of_degree_lt <|
                    (degree_add_le _ _).trans_lt <|
                      max_lt_iff.mpr ⟨hdpq.trans_lt _, hdq.trans_lt _⟩).trans
                (max_eq_left_of_lt _).symm <;> rw [hdp] <;>
                exact WithBot.coe_lt_coe.mpr <| by dsimp; linarith only [hpq]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ C
        ((W.preΨ (m + 2) * W.preΨ m ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) -
          W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2) *
      1 =
    (C (W.preΨ (m + 2)) * if Even m then W.ψ₂ else 1) * (C (W.preΨ m) * if Even m then W.ψ₂ else 1) ^ 3 -
        (C (W.preΨ (m - 1)) * if ¬Even m then W.ψ₂ else 1) * (C (W.preΨ (m + 1)) * if ¬Even m then W.ψ₂ else 1) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) *
        C (if Even m then W.preΨ (m + 2) * W.preΨ m ^ 3 else -W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3)

Tactic:
split_ifs <;> C_simp <;> rw [C_Ψ₂Sq]

Goal state after:
case pos
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : Even m
⊢ (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3 * (W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial) ^ 2 -
        C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3 * 1) *
      1 =
    C (W.preΨ (m + 2)) * W.ψ₂ * (C (W.preΨ m) * W.ψ₂) ^ 3 - C (W.preΨ (m - 1)) * 1 * (C (W.preΨ (m + 1)) * 1) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3)

case neg
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : ¬Even m
⊢ (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3 * 1 -
        C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3 * (W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial) ^ 2) *
      1 =
    C (W.preΨ (m + 2)) * 1 * (C (W.preΨ m) * 1) ^ 3 - C (W.preΨ (m - 1)) * W.ψ₂ * (C (W.preΨ (m + 1)) * W.ψ₂) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) *
        (-C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : IsAffine X
inst✝² : ∀ (i : I), IsAffine (D.obj i)
a : c.pt ⟶ X
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
f✝ : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f✝
inst✝ : IsAffine (Spec R)
ha : c.π ≫ t = (Functor.const I).map (a ≫ f✝)
this :
  ∀ {X : Scheme} [IsAffine X] (a : c.pt ⟶ X) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f],
    c.π ≫ t = (Functor.const I).map (a ≫ f) → (∃ S, X = Spec S) → ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i
hX : ¬∃ S, X = Spec S
i : I
f : D.obj i ⟶ Spec Γ(X, ⊤)
hf : c.π.app i ≫ f = a ≫ X.isoSpec.hom ∧ f ≫ X.isoSpec.inv ≫ f✝ = t.app i
⊢ c.π.app i ≫ f ≫ X.isoSpec.inv = a ∧ (f ≫ X.isoSpec.inv) ≫ f✝ = t.app i

Tactic:
by simpa [← Iso.comp_inv_eq] using! hf

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

Goal state before:
pp: case inl
n : ℕ
hn : 2 * n ≠ 0
⊢ 2 * ↑(expDegree (2 * n)) = ↑(2 * n) ^ 2 - if Even (2 * n) then 4 else 1

pp: case inr
n : ℕ
hn : 2 * n + 1 ≠ 0
⊢ 2 * ↑(expDegree (2 * n + 1)) = ↑(2 * n + 1) ^ 2 - if Even (2 * n + 1) then 4 else 1

Tactic:
· rcases n with _ | n
    · contradiction
    push_cast [expDegree, show (2 * (n + 1)) ^ 2 = 2 * (2 * n * (n + 2)) + 4 by ring1, even_two_mul,
      Nat.add_sub_cancel, Nat.mul_div_cancel_left _ two_pos]
    ring1

Goal state after:
case inr
n : ℕ
hn : 2 * n + 1 ≠ 0
⊢ 2 * ↑(expDegree (2 * n + 1)) = ↑(2 * n + 1) ^ 2 - if Even (2 * n + 1) then 4 else 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ W.Δ = -W.a₂ ^ 3 * W.a₆

Tactic:
by
  rw [Δ_of_isCharThreeJNeZeroNF]
  linear_combination (-21 * W.a₂ ^ 3 * W.a₆ - 144 * W.a₆ ^ 2) * CharP.cast_eq_zero R 3

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

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P x * ![P x / P z ^ 2, P y / P z ^ 3, 1] z ^ 2 + -P x * 1 -
      (![P x / P z ^ 2, P y / P z ^ 3, 1] x * P z ^ 2 + -P x * (P z ^ 2 / P z ^ 2)) =
    0

Tactic:
(matrix_simp; ring1)

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

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P y * ![P x / P z ^ 2, P y / P z ^ 3, 1] z ^ 3 + -P y * 1 -
      (![P x / P z ^ 2, P y / P z ^ 3, 1] y * P z ^ 3 + -P y * (P z ^ 3 / P z ^ 3)) =
    0

Tactic:
(matrix_simp; ring1)

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.dblU (u • P) = u ^ 4 * W'.dblU P

Tactic:
simp only [dblU_eq, smul_fin3_ext]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.a₁ * (u ^ 3 * P y) * (u * P z) -
      (3 * (u ^ 2 * P x) ^ 2 + 2 * W'.a₂ * (u ^ 2 * P x) * (u * P z) ^ 2 + W'.a₄ * (u * P z) ^ 4) =
    u ^ 4 * (W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.neg (u • P) = u • W'.neg P

Tactic:
neg,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ ![(u • P) x, W'.negY (u • P), (u • P) z] = u • W'.neg P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.neg P = ![P x, -P y, 0]

Tactic:
neg,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ ![P x, W'.negY P, P z] = ![P x, -P y, 0]
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
⊢ W.neg P = P z • ![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]

Tactic:
neg,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ![P x, W.negY P, P z] = P z • ![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case mk.mk.h₁
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)
⊢ x✝¹ * x✝ * ↑(y✝ * y✝¹) ≤ᵥ x✝ * x✝¹ * ↑(y✝¹ * y✝)

Tactic:
simp only [Submonoid.coe_mul]
      nth_grw 2 [veq_mul_comm]
      nth_grw 6 [veq_mul_comm]

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

Goal state before:
pp: case h₂
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)
⊢ x✝ * x✝¹ * ↑(y✝¹ * y✝) ≤ᵥ x✝¹ * x✝ * ↑(y✝ * y✝¹)

Tactic:
simp only [Submonoid.coe_mul]
      nth_grw 2 [veq_mul_comm]
      nth_grw 6 [veq_mul_comm]

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

Goal state before:
pp: case neg
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure[topologicalSpace] s) t
h₂ : Disjoint s (closure[topologicalSpace] t)
hs : 0 ∉ s
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
(isOpen_iff.2 (.inl hs)).nhdsSet_eq,

Goal state after:
case neg
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure[topologicalSpace] s) t
h₂ : Disjoint s (closure[topologicalSpace] t)
hs : 0 ∉ s
⊢ Disjoint (𝓟 s) (𝓝ˢ t)
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ Continuous[instTopologicalSpaceProd, topologicalSpace] fun p ↦ p.1 * p.2

Tactic:
simp only [continuous_iff_continuousAt, ContinuousAt]

Goal state after:
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ ∀ (x : Γ₀ × Γ₀), Tendsto (fun p ↦ p.1 * p.2) (𝓝 x) (𝓝 (x.1 * x.2))
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case h₂
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ ↑t * ↑⟨x, hx⟩ ≤ᵥ ↑s * ↑⟨y, hy⟩

Tactic:
· grw [veq_mul_comm, veq_mul_comm _ y]
        simpa [mul_comm] using h₁

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

Goal state before:
pp: K : Type u_2
inst✝¹ : DivisionRing K
inst✝ : ValuativeRel K
a : K
⊢ a = 0 → a =ᵥ 0

Tactic:
by simp +contextual

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

Goal state before:
pp: M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : IsUniformAddGroup α
n : ℕ
a✝ : Completion α
a : α
⊢ Int.negSucc n • ↑a = -(↑n.succ • ↑a)

Tactic:
rw [← coe_smul, show (Int.negSucc n) • a = -((n.succ : ℤ) • a) from
            SubNegMonoid.zsmul_neg' n a, coe_neg, coe_smul]

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
I : Ideal R
hI : Maximal (fun x ↦ ¬P x) I
⊢ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
by
    by_contra! ⟨a, b, hab, ha, hb⟩
    have h₁ : P (I ⊔ span {a}) := of_not_not <| hI.not_prop_of_gt (Submodule.lt_sup_iff_notMem.2 ha)
    have h₂ : P (I.colon (span {a})) := of_not_not <| hI.not_prop_of_gt <| lt_of_le_of_ne le_colon
      (fun H ↦ hb <| H ▸ mem_colon_span_singleton.2 (mul_comm a b ▸ hab))
    exact hI.prop (hP.oka h₁ h₂)

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

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
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 | v.restrict (y - x) < ↑γ} ⊆ Inv.inv ⁻¹' s

Tactic:
use min (γ * (γ' * γ')) γ'

Goal state after:
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₀ˣ := ⋯
⊢ {y | v.restrict (y - x) < ↑(min (γ * (γ' * γ')) γ')} ⊆ Inv.inv ⁻¹' s
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ ∃ c, Tendsto (⇑v.restrict) (Filter.comap Completion.coe' (𝓝 0)) (𝓝 c)

Tactic:
refine ⟨0, ?_⟩

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Tendsto (⇑v.restrict) (Filter.comap Completion.coe' (𝓝 0)) (𝓝 0)
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 Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x ↦ x * x₀⁻¹) fun x ↦ x * x₀
x : hat K
⊢ (fun x ↦ x * x₀) ((fun x ↦ x * x₀⁻¹) x) = x

Tactic:
simp only [mul_assoc, inv_mul_cancel₀ h, mul_one]

Goal state after:
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 | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃+o ℤ)

Tactic:
suffices Set.WellFoundedOn {x : G | 0 ≤ x} (· < ·) ↔ Nonempty (G ≃+o ℤ) by
    rw [← this]
    refine ⟨fun h ↦ (h.mapsTo (· + g) ?_).mono' ?_, fun h ↦ (h.mapsTo (· - g) ?_).mono' ?_⟩ <;>
    · try intro
      simp [Function.onFun]
  constructor
  · intro h
    replace h : WellFounded (α := {x : G | 0 ≤ x}) (· < ·) := h
    rw [WellFounded.wellFounded_iff_has_min] at h
    by_cases! H : ∀ (x : G) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y -- Archimedean
    · replace H : Archimedean G := ⟨H⟩
      rw [LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered]
      intro hd
      obtain ⟨y, hy⟩ := exists_ne (0 : G)
      wlog! hy' : 0 < y generalizing y
      · refine this (-y) ?_ ?_
        · simp [hy]
        · simp [lt_of_le_of_ne hy' hy]
      obtain ⟨⟨z, hz⟩, hz', hz''⟩ := h ({x | ⟨0, le_rfl⟩ < x}) ⟨⟨y, hy'.le⟩, hy'⟩
      obtain ⟨w, hw, hw'⟩ := exists_between hz'
      exact hz'' ⟨w, hw.le⟩ hw hw'
    · exfalso
      obtain ⟨x, y, hy0, H⟩ := H
      obtain ⟨_, ⟨n, rfl⟩, hz⟩ :=
        h (Set.range (fun n : ℕ ↦ ⟨x - n • y, sub_nonneg.mpr (H _).le⟩)) (range_nonempty _)
      refine hz ⟨x - (n + 1) • y, sub_nonneg.mpr (H _).le⟩ ⟨_, rfl⟩ ?_
      simp [add_smul, hy0]
  · rintro ⟨f⟩
    have : LocallyFiniteOrder G := LocallyFiniteOrder.ofOrderIsoClass f
    exact BddBelow.wellFoundedOn_lt ⟨0, by simp [mem_lowerBounds]⟩

Goal state after: