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:
simp [O]

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

Goal state before:
pp: R : Type u_6
inst✝ : CommRing R
M : Submodule ℤ R
hM : 1 ∈ M
S : ConstructibleSetData R[X]
hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M
f : BasicConstructibleSetData R[X] → ConstructibleSetData R
hf₁ :
  ∀ (C : BasicConstructibleSetData R[X]),
    comap Polynomial.C '' (zeroLocus (Set.range { val := C.g }.val) \ zeroLocus {C.f}) = (f C).toSet
hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g }.degBound
hf₃ :
  ∀ (C : BasicConstructibleSetData R[X]),
    ∀ C_1 ∈ f C, ∀ (i : Fin C_1.n), C_1.g i ∈ coeffSubmodule ℤ { val := C.g } ^ { val := C.g }.powBound
x : BasicConstructibleSetData R
y : BasicConstructibleSetData R[X]
hy : y ∈ S
hx : x ∈ f y
H : { val := y.g }.degBound ≤ S.degBound
i : Fin x.n
h : S.degBound = 0
⊢ { val := y.g }.degBound = 0

Tactic:
nlinarith

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ (W.map f).polynomialX = Polynomial.map (mapRingHom f) W.polynomialX

Tactic:
simp only [polynomialX]
  map_simp

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective ⇑f
y : W'.CoordinateRing
hy : (map W' f) y = 0
⊢ y = 0

Tactic:
by
    obtain ⟨p, q, rfl⟩ := exists_smul_basis_eq y
    simp_rw [map_add, CoordinateRing.map_smul, map_one, map_mk, map_X] at hy
    obtain ⟨hp, hq⟩ := smul_basis_eq_zero hy
    rw [Polynomial.map_eq_zero_iff hf] at hp hq
    simp_rw [hp, hq, zero_smul, add_zero]

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

Goal state before:
pp: case inl
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
hx : W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0
⊢ ∃ a a_1 a_2 a_3,
    a_3 * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
      1 + a * C (X - C x) + a_1 * (Y - C (C y)) + a_2 * (Y - C (C (W.negY x y)))

pp: case inr
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
hy : 2 * y + W.a₁ * x + W.a₃ ≠ 0
⊢ ∃ a a_1 a_2 a_3,
    a_3 * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
      1 + a * C (X - C x) + a_1 * (Y - C (C y)) + a_2 * (Y - C (C (W.negY x y)))

Tactic:
· let W_X := W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)
    refine
      ⟨C <| C W_X⁻¹ * -(X + C (2 * x + W.a₂)), C <| C <| W_X⁻¹ * W.a₁, 0, C <| C <| W_X⁻¹ * -1, ?_⟩
    rw [← mul_right_inj' <| C_ne_zero.mpr <| C_ne_zero.mpr hx]
    simp only [W_X, mul_add, ← mul_assoc, ← C_mul, mul_inv_cancel₀ hx]
    C_simp
    ring1

Goal state after:
case inr
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
hy : 2 * y + W.a₁ * x + W.a₃ ≠ 0
⊢ ∃ a a_1 a_2 a_3,
    a_3 * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
      1 + a * C (X - C x) + a_1 * (Y - C (C y)) + a_2 * (Y - C (C (W.negY x y)))
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
simp_rw [normEDS, mul_right_comm, preNormEDS_mul_complEDS₂, mul_assoc, apply_ite₂, one_mul,
    mul_one, ite_self, if_pos <| even_two_mul k]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
inst✝ : c.pt.IsQuasiAffine
i : ↥c.pt → I
f : (x : ↥c.pt) → ↑Γ(D.obj (i x), ⊤)
hf : ∀ (x : ↥c.pt), IsAffineOpen ((D.obj (i x)).basicOpen (f x))
hi : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ (D.obj (i x)).basicOpen (f x)
σ : Finset ↥c.pt
hσ : ⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier = ⊤
σi : ↥c.pt → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi : ∀ (x : ↥c.pt), x ∈ (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))).carrier
j : I
fj : (i_1 : I) → i_1 ∈ Finset.image i σ → (j ⟶ i_1)
x : ↥(((Functor.const I).obj c.pt).obj j)
x✝ : x ∈ ⊤
⊢ (c.π.app j) x ∈ D.map (fj (i (σi x)) ⋯) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))

Tactic:
change (c.π.app j ≫ D.map _).base x ∈ (D.obj (i (σi x))).basicOpen (f (σi x))

Goal state after:
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)
inst✝ : c.pt.IsQuasiAffine
i : ↥c.pt → I
f : (x : ↥c.pt) → ↑Γ(D.obj (i x), ⊤)
hf : ∀ (x : ↥c.pt), IsAffineOpen ((D.obj (i x)).basicOpen (f x))
hi : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ (D.obj (i x)).basicOpen (f x)
σ : Finset ↥c.pt
hσ : ⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier = ⊤
σi : ↥c.pt → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi : ∀ (x : ↥c.pt), x ∈ (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))).carrier
j : I
fj : (i_1 : I) → i_1 ∈ Finset.image i σ → (j ⟶ i_1)
x : ↥(((Functor.const I).obj c.pt).obj j)
x✝ : x ∈ ⊤
⊢ (c.π.app j ≫ D.map (fj (i (σi x)) ⋯)) x ∈ (D.obj (i (σi x))).basicOpen (f (σi x))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
x✝¹ x✝ : W.Point
⊢ toClass (x✝¹ + x✝) = toClass (x✝ + x✝¹)

Tactic:
by simp only [map_add, add_comm]

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

Goal state before:
pp: case some.some
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K
inst✝¹³ : Field L
W' : Affine R
W : Affine F
inst✝¹² : DecidableEq F
inst✝¹¹ : DecidableEq K
inst✝¹⁰ : DecidableEq L
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x₁ y₁ : F
h₁ : (W'⁄F).Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
⊢ (match some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => some (f x) (f y) ⋯) =
    (match some x₁ y₁ h₁ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯) +
      match some x₂ y₂ h₂ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯

Tactic:
by_cases hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂

Goal state after:
case pos
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K
inst✝¹³ : Field L
W' : Affine R
W : Affine F
inst✝¹² : DecidableEq F
inst✝¹¹ : DecidableEq K
inst✝¹⁰ : DecidableEq L
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x₁ y₁ : F
h₁ : (W'⁄F).Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂
⊢ (match some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => some (f x) (f y) ⋯) =
    (match some x₁ y₁ h₁ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯) +
      match some x₂ y₂ h₂ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯

case neg
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K
inst✝¹³ : Field L
W' : Affine R
W : Affine F
inst✝¹² : DecidableEq F
inst✝¹¹ : DecidableEq K
inst✝¹⁰ : DecidableEq L
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x₁ y₁ : F
h₁ : (W'⁄F).Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂)
⊢ (match some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => some (f x) (f y) ⋯) =
    (match some x₁ y₁ h₁ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯) +
      match some x₂ y₂ h₂ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁶ : Category.{u, u} I
inst✝⁵ : IsCofiltered I
R : CommRingCat
inst✝⁴ : IsAffine (Spec R)
S : CommRingCat
inst✝³ : IsAffine (Spec S)
φ : R ⟶ S
inst✝² : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst✝¹ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
a : c.pt ⟶ Spec S
e : ((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec ≅ (Functor.const I).obj (Spec R) :=
  NatIso.ofComponents (fun x ↦ Iso.refl ((((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec).obj x)) ⋯
t : (Functor.const Iᵒᵖ).obj R ⟶ D.leftOp
ha : c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom = (Functor.const I).map (a ≫ Spec.map φ)
this✝ :
  ∀ (c : Cone (D ⋙ Scheme.Spec)) (hc : IsLimit c) (a : c.pt ⟶ Spec S),
    c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom = (Functor.const I).map (a ≫ Spec.map φ) →
      (∃ c', c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')) →
        ∃ i g,
          c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
hc' : ¬∃ c', c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')
inst✝ : IsAffine c.pt
e' : (D ⋙ Scheme.Spec).op ⋙ Γ ≅ D.leftOp := D.leftOp.isoWhiskerLeft SpecΓIdentity
c' : Cone D := coneOfCoconeLeftOp ((Cocone.precompose e'.inv).obj (Γ.mapCocone c.op))
inst : ∀ (i : Iᵒᵖ), IsAffine (Opposite.unop ((D ⋙ Scheme.Spec).op.obj i))
i : I
this : c.π.app i ≫ Spec.map (t.app (Opposite.op i)) = a ≫ Spec.map φ
⊢ ((Scheme.Spec.mapCone c').π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i =
    ((Functor.const I).map ((c.pt.isoSpec.inv ≫ a) ≫ Spec.map φ)).app i

Tactic:
simp [c', e, e', ← this, Iso.eq_inv_comp, isoSpec_hom_naturality_assoc]

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
⊢ (W.map f).Ψ₂Sq = Polynomial.map f W.Ψ₂Sq

Tactic:
simp [Ψ₂Sq, map_ofNat]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ 2 * W.a₄ + W.a₁ * W.a₃ = 2 * W.a₄

Tactic:
a₁_of_isCharTwoJEqZeroNF

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ 2 * W.a₄ + 0 * W.a₃ = 2 * W.a₄
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hz : P z = Q z
hQz : Q z ∈ nonZeroDivisors R
⊢ P ≈ Q → P = Q

Tactic:
rintro ⟨u, rfl⟩

Goal state after:
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
hQz : Q z ∈ nonZeroDivisors R
u : Rˣ
hz : (fun m ↦ m • Q) u z = Q z
⊢ (fun m ↦ m • Q) u = Q
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
heq : E.j = E'.j
⊢ ∃ C, C • E = E'

Tactic:
by
  obtain ⟨C, _ | _⟩ := E.exists_variableChange_isCharThreeNF
  · obtain ⟨C', _ | _⟩ := E'.exists_variableChange_isCharThreeNF
    · rw [← variableChange_j E C, ← variableChange_j E' C'] at heq
      obtain ⟨C'', hC⟩ := exists_variableChange_of_char_three_of_j_ne_zero _ _ heq
      use C'⁻¹ * C'' * C
      rw [mul_smul, mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]
    · have h := (C • E).j_ne_zero_of_isCharThreeJNeZeroNF_of_char_three
      rw [variableChange_j, heq, ← variableChange_j E' C', j_of_isShortNF_of_char_three] at h
      exact False.elim (h rfl)
  · obtain ⟨C', _ | _⟩ := E'.exists_variableChange_isCharThreeNF
    · have h := (C' • E').j_ne_zero_of_isCharThreeJNeZeroNF_of_char_three
      rw [variableChange_j, ← heq, ← variableChange_j E C, j_of_isShortNF_of_char_three] at h
      exact False.elim (h rfl)
    · obtain ⟨C'', hC⟩ := exists_variableChange_of_char_three_of_j_eq_zero (C • E) (C' • E')
      use C'⁻¹ * C'' * C
      rw [mul_smul, mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]

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

Tactic:
Nat.div_pos_iff,

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < n
h : ↑n ≠ 0
⊢ 0 < 2 ∧ 2 ≤ n ^ 2 - if Even n then 4 else 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

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

Tactic:
simp_rw [preΨ_neg, coeff_neg, Int.natAbs_neg, even_neg]

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = ↑(if Even ↑n then ↑n / 2 else ↑n)
n : ℕ
⊢ -(W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = ↑(if Even ↑n then -↑n / 2 else -↑n)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

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

Tactic:
have hu0 : u ≠ 0 := by
    rw [← pow_ne_zero_iff four_ne_zero, hu4, div_ne_zero_iff]
    exact ⟨ha₄, ha₄'⟩

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

Goal state before:
pp: case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ P ≈ Q

Tactic:
refine equiv_of_X_eq_of_Y_eq ((map_ne_zero_iff f f.injective).mp hz)
        ((map_ne_zero_iff f f.injective).mp <| hz.comp (Z_eq_zero_of_equiv h).mpr) ?_ ?_
      all_goals apply f.injective; map_simp
      exacts [X_eq_of_equiv h, Y_eq_of_equiv h]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.neg P ≈ W'.neg Q

Tactic:
rcases h with ⟨u, rfl⟩
  exact neg_smul_equiv Q u.isUnit

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_1
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✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
this✝¹ : ∀ (i : I), CompactSpace ↥((D ⋙ Over.forget S).obj i)
this✝ : ∀ (i : I), QuasiSeparatedSpace ↥((D ⋙ Over.forget S).obj i)
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Over.forget S).map f)
k : Iᵒᵖ
g₁ g₂ : (D.op ⋙ yoneda.obj X).obj k
hg :
  ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).ι k g₁ =
    ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).ι k g₂
⊢ ∃ k_1 f,
    (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map f)) g₁ = (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map f)) g₂

Tactic:
obtain ⟨k, hik, heq⟩ := Scheme.exists_hom_comp_eq_comp_of_locallyOfFiniteType
        (D ⋙ Over.forget _) (.mk (fun _ ↦ (D.obj _).hom)) X.hom _ (isLimitOfPreserves _ hc.unop)
        g₁.left g₂.left (Over.w g₁).symm (Over.w g₂).symm congr($(hg).left)

Goal state after:
case refine_1
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✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
this✝¹ : ∀ (i : I), CompactSpace ↥((D ⋙ Over.forget S).obj i)
this✝ : ∀ (i : I), QuasiSeparatedSpace ↥((D ⋙ Over.forget S).obj i)
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Over.forget S).map f)
k✝ : Iᵒᵖ
g₁ g₂ : (D.op ⋙ yoneda.obj X).obj k✝
hg :
  ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).ι k✝ g₁ =
    ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).ι k✝ g₂
k : I
hik : k ⟶ Opposite.unop k✝
heq : (D ⋙ Over.forget S).map hik ≫ Over.Hom.left g₁ = (D ⋙ Over.forget S).map hik ≫ Over.Hom.left g₂
⊢ ∃ k f,
    (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map f)) g₁ = (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map f)) g₂
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: e : ℝ≥0
he : e ≠ 0
⊢ (if hx : 1 = 0 then 0 else e ^ toAdd (unzero hx)) = 1

Tactic:
rw [dif_neg one_ne_zero, unzero_coe (x := 1), toAdd_one, zpow_zero]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y : R
hx : 0 <ᵥ x
hy : 0 <ᵥ y
⊢ 0 <ᵥ x * y

Tactic:
by
  contrapose hy
  rw [not_vlt] at hy ⊢
  grw [show (0 : R) = x * 0 by simp, veq_mul_comm, veq_mul_comm x] at hy
  exact vle_mul_cancel hx hy

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

Goal state before:
pp: case zero
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
⊢ (fromAffine 0).toAffineLift = 0

Tactic:
fromAffine_zero,

Goal state after:
case zero
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
⊢ toAffineLift 0 = 0
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 : ValueGroupWithZero R
hab : a ≤ b
c : ValueGroupWithZero R
⊢ a * c ≤ b * c

Tactic:
induction a using ValueGroupWithZero.ind
    induction b using ValueGroupWithZero.ind
    induction c using ValueGroupWithZero.ind
    simp only [ValueGroupWithZero.mk_mul_mk, ValueGroupWithZero.mk_le_mk, Submonoid.coe_mul]
    nth_grw 1 [veq_mul_mul_mul_comm]
    nth_grw 2 [veq_mul_mul_mul_comm]
    exact mul_vle_mul_left hab _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
r s : (ValueGroupWithZero R)ˣ
h : r ≠ s
hr : r ≠ 1
⊢ ↑r ≠ 1

Tactic:
by simpa using hr

Goal state after: