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
⊢ ∃ k hik, D.map hik ≫ a = D.map hik ≫ b

Tactic:
classical
  have := isAffineHom_π_app _ _ hc
  let A : ExistsHomHomCompEqCompAux D t f :=
    { c := c, hc := hc, i := i, a := a, ha := ha, b := b, hb := hb, hab := hab
      𝒰S := S.affineCover, 𝒰X i := Scheme.affineCover _ }
  let 𝒰 := Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X
  let W := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
  choose k hki' heq using A.exists_eq
  let 𝒰Df := A.𝒰D.finiteSubcover
  rcases isEmpty_or_nonempty (D.obj A.i') with h | h
  · exact ⟨A.i', A.hii', isInitialOfIsEmpty.hom_ext _ _⟩
  let O : Finset I := {A.i'} ∪ Finset.univ.image (fun i : 𝒰Df.I₀ ↦ k <| A.𝒰D.idx i.1)
  let o := Nonempty.some (inferInstance : Nonempty 𝒰Df.I₀)
  have ho : k (A.𝒰D.idx o.1) ∈ O := by
    simp [O]
  obtain ⟨l, hl1, hl2⟩ := IsCofiltered.inf_exists O
    (Finset.univ.image (fun i : 𝒰Df.I₀ ↦
      ⟨k <| A.𝒰D.idx i.1, A.i', by simp [O], by simp [O], hki' <| A.𝒰D.idx i.1⟩))
  have (w v : 𝒰Df.I₀) :
      hl1 (by simp [O]) ≫ hki' (A.𝒰D.idx w.1) = hl1 (by simp [O]) ≫ hki' (A.𝒰D.idx v.1) := by
    trans hl1 (show A.i' ∈ O by simp [O])
    · exact hl2 _ _ (Finset.mem_image_of_mem _ (Finset.mem_univ _))
    · exact .symm <| hl2 _ _ (Finset.mem_image_of_mem _ (by simp))
  refine ⟨l, hl1 ho ≫ hki' _ ≫ A.hii', ?_⟩
  apply Cover.hom_ext (𝒰Df.pullback₁ (D.map <| hl1 ho ≫ hki' _))
  intro u
  let F : pullback (D.map (hl1 ho ≫ hki' (A.𝒰D.idx o.1))) (𝒰Df.f u) ⟶
      pullback (D.map (hki' <| A.𝒰D.idx u.1)) (A.𝒰D.f <| A.𝒰D.idx u.1) :=
    pullback.map _ _ _ _ (D.map <| hl1 (by simp [O]))
      (𝟙 _) (𝟙 _) (by rw [Category.comp_id, ← D.map_comp, this]) rfl
  have hF : F ≫ pullback.fst (D.map (hki' _)) (A.𝒰D.f _) =
      pullback.fst _ _ ≫ D.map (hl1 (by simp [O])) := by simp [F]
  simp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
    PreZeroHypercover.pullback₁_X, PreZeroHypercover.pullback₁_f, Functor.map_comp, Category.assoc]
    at heq ⊢
  simp_rw [← D.map_comp_assoc, reassoc_of% this o u, D.map_comp_assoc]
  rw [← reassoc_of% hF, ← reassoc_of% hF, heq]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0 ∧
      (evalEval x y W.polynomialX ≠ 0 ∨ evalEval x y W.polynomialY ≠ 0) ↔
    y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0 ∧
      (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)

Tactic:
evalEval_polynomialX,

Goal state after:
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0 ∧
      (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ evalEval x y W.polynomialY ≠ 0) ↔
    y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0 ∧
      (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
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₂
⊢ (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁) =
    -evalEval x₁ y₁ W.polynomialX / evalEval x₁ y₁ W.polynomialY

Tactic:
evalEval_polynomialX,

Goal state after:
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₂
⊢ (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁) =
    -(W.a₁ * y₁ - (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄)) / evalEval x₁ y₁ W.polynomialY
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case left.inl
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)
hg'' : ∀ (t : Set (PrimeSpectrum (MvPolynomial (Fin m) R))), comap g '' t = comap σ ⁻¹' t ∩ zeroLocus s₀
hS' : comap g '' S.toSet = S'.toSet
x : BasicConstructibleSetData (MvPolynomial (Fin m) R)
hx : x ∈ S
i : Fin m →₀ ℕ
j : Fin x.n
⊢ (MvPolynomial.coeff i
        (Sum.elim (⇑σ ∘ x.g) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i)))
          (Sum.inl j))).degrees ≤
    Finset.univ.val

Tactic:
simp [σ, MvPolynomial.coeff_map, degrees_C]

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
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : U ∈ (D.obj i).affineOpens
hxU : (c.π.app i) x ∈ ↑U
j : I
r : ↑Γ(D.obj j, ⊤)
hr : IsAffineOpen (c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hxr : x ∈ ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hrU : ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r)) ⊆ ↑(c.π.app i ⁻¹ᵁ U)
k : I
fki : k ⟶ i
fkj : k ⟶ j
l : I
flk : l ⟶ k
hl :
  D.map flk ⁻¹ᵁ (D.obj k).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map fkj))) r) ≤ D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ U
⊢ (D.obj l).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map flk ≫ D.map fkj))) r) ≤ D.map (flk ≫ fki) ⁻¹ᵁ U

Tactic:
elementwise_of% Scheme.Hom.comp_appTop,

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
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : U ∈ (D.obj i).affineOpens
hxU : (c.π.app i) x ∈ ↑U
j : I
r : ↑Γ(D.obj j, ⊤)
hr : IsAffineOpen (c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hxr : x ∈ ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hrU : ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r)) ⊆ ↑(c.π.app i ⁻¹ᵁ U)
k : I
fki : k ⟶ i
fkj : k ⟶ j
l : I
flk : l ⟶ k
hl :
  D.map flk ⁻¹ᵁ (D.obj k).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map fkj))) r) ≤ D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ U
⊢ (D.obj l).basicOpen
      ((ConcreteCategory.hom (Hom.appTop (D.map flk))) ((ConcreteCategory.hom (Hom.appTop (D.map fkj))) r)) ≤
    D.map (flk ≫ fki) ⁻¹ᵁ U
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ (ClassGroup.mk W.FunctionField) (XYIdeal' ⋯) * (ClassGroup.mk W.FunctionField) (XYIdeal' h) = 1

Tactic:
rw [← map_mul]

Goal state after:
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ (ClassGroup.mk W.FunctionField) (XYIdeal' ⋯ * XYIdeal' h) = 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ (ClassGroup.mk W.FunctionField) (XYIdeal' h₁) * (ClassGroup.mk W.FunctionField) (XYIdeal' h₂) =
    (ClassGroup.mk W.FunctionField) (XYIdeal' ⋯)

Tactic:
rw [← map_mul]

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ (ClassGroup.mk W.FunctionField) (XYIdeal' h₁ * XYIdeal' h₂) = (ClassGroup.mk W.FunctionField) (XYIdeal' ⋯)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: 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
⊢ ((Algebra.norm R[X]) (p • 1 + q • (mk W') Y)).degree = max (2 • p.degree) (2 • q.degree + 3)

Tactic:
have hdq :
      (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3 := by
    rw [degree_mul, degree_pow, ← one_mul <| X ^ 3, ← C_1, degree_cubic <| one_ne_zero' R]

Goal state after:
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
⊢ ((Algebra.norm R[X]) (p • 1 + q • (mk W') Y)).degree = max (2 • p.degree) (2 • q.degree + 3)
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✝¹ : Nontrivial R
inst✝ : WeierstrassCurve.IsElliptic W'
p : W'.Point → Prop
p0 : p Point.zero
⊢ (fun xy ↦ ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h)) = fun xy ↦
    ∃ (h : W'.Equation xy.1 xy.2), p (Point.mk h)

Tactic:
by ext; simp [equation_iff_nonsingular, Point.mk]

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

Goal state before:
pp: case mp.some
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x✝ y✝ : F
h : W.Equation x✝ y✝
right✝ : evalEval x✝ y✝ W.polynomialX ≠ 0 ∨ evalEval x✝ y✝ W.polynomialY ≠ 0
hP : toClass (some x✝ y✝ ⋯) = 0
⊢ some x✝ y✝ ⋯ = 0

Tactic:
rcases (ClassGroup.mk_eq_one_of_coe_ideal <| by rfl).mp hP with ⟨p, h0, hp⟩
      apply (p.natDegree_norm_ne_one _).elim
      rw [← finrank_quotient_span_eq_natDegree_norm (CoordinateRing.basis W) h0,
        ← (quotientEquivAlgOfEq F hp).toLinearEquiv.finrank_eq,
        (CoordinateRing.quotientXYIdealEquiv h).toLinearEquiv.finrank_eq, Module.finrank_self]

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
inst✝ : CharP R 2
⊢ W.b₄ = 0

Tactic:
by
  rw [b₄_of_isCharTwoJEqZeroNF]
  linear_combination W.a₄ * CharP.cast_eq_zero R 2

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_3
I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
i' : I
fi'i : i' ⟶ i
hi' : ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2
𝒱' : ↥s → (D.obj i').Opens := fun x ↦ D.map fi'i ⁻¹ᵁ 𝒱 x
h𝒱'𝒰 : ∀ (j : ↥s), c.π.app i' ⁻¹ᵁ 𝒱' j = (↑↑j).1
x✝ : ∀ (j : ↥s) (k : Over i'), IsAffine ((opensDiagram D i' (𝒱' j)).obj k)
t𝒱 : (j : ↥s) → opensDiagram D i' (𝒱' j) ⟶ (Functor.const (Over i')).obj ↑↑(↑(↑↑j).2).2 :=
  fun j ↦ { app := fun k ↦ Hom.resLE (t.app k.left) (↑(↑(↑↑j).2).2) (D.map k.hom ⁻¹ᵁ 𝒱' j) ⋯, naturality := ⋯ }
this : ∀ (j : ↥s), IsAffine ↑(↑(↑↑j).2).1
k : ↥s → Over i'
ak : (j : ↥s) → (opensDiagram D i' (𝒱' j)).obj (k j) ⟶ ↑(↑(↑↑j).2).1
hk : ∀ (j : ↥s), (opensCone D c i' (𝒱' j)).π.app (k j) ≫ ak j = Hom.resLE a (↑(↑↑j).2).1 (c.π.app i' ⁻¹ᵁ 𝒱' j) ⋯
hk' : ∀ (j : ↥s), ak j ≫ Hom.resLE f (↑(↑(↑↑j).2).2) (↑(↑↑j).2).1 ⋯ = (t𝒱 j).app (k j)
i'' : I
fi''i' : i'' ⟶ i'
fi'' : (x : ↥s) → i'' ⟶ (k x).left
hi'' : ∀ (x : ↥s), fi'' x ≫ (k x).hom = fi''i'
j : ↥s
e : c.π.app i'' ⁻¹ᵁ D.map (fi''i' ≫ fi'i) ⁻¹ᵁ 𝒱 j ≤ c.π.app i' ⁻¹ᵁ 𝒱' j
⊢ c.π.app i'' ∣_ D.map (fi''i' ≫ fi'i) ⁻¹ᵁ 𝒱 j ≫
      (D.obj i'').homOfLE ⋯ ≫ D.map (fi'' j) ∣_ D.map (k j).hom ⁻¹ᵁ 𝒱' j ≫ ak j ≫ Opens.ι (↑(↑↑j).2).1 =
    (c.π.app i'' ⁻¹ᵁ D.map (fi''i' ≫ fi'i) ⁻¹ᵁ 𝒱 j).ι ≫ a

Tactic:
simpa [← AlgebraicGeometry.Scheme.Hom.resLE_eq_morphismRestrict,
        Scheme.Hom.resLE_comp_resLE_assoc] using! congr(Scheme.homOfLE _ e ≫ $(hk j) ≫ Opens.ι _)

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : Nontrivial R
⊢ W'.Nonsingular ![1, 1, 0]

Tactic:
simp only [nonsingular_of_Z_eq_zero, equation_zero, true_and, fin3_def_ext, ← not_and_or]
  exact fun h => one_ne_zero <| by linear_combination (norm := ring1) h.1 - h.2.1

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ W.neg P = -(P y / P x) • ![1, 1, 0]

Tactic:
have hX {n : ℕ} : IsUnit <| P x ^ n := (isUnit_X_of_Z_eq_zero hP hPz).pow n

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ W.neg P = -(P y / P x) • ![1, 1, 0]
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: e : ℝ≥0
he : e ≠ 0
⊢ e ^ 0 = 1

Tactic:
zpow_zero

Goal state after:
e : ℝ≥0
he : e ≠ 0
⊢ 1 = 1
Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : NonarchimedeanGroup G
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × K)
hU : ∃ t₁ ∈ 𝓝 1.1, ∃ t₂ ∈ 𝓝 1.2, t₁ ×ˢ t₂ ⊆ U
⊢ ∃ V W, ↑V ×ˢ ↑W ⊆ U

Tactic:
rcases hU with ⟨U₁, hU₁, U₂, hU₂, h⟩

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : NonarchimedeanGroup G
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × K)
U₁ : Set G
hU₁ : U₁ ∈ 𝓝 1.1
U₂ : Set K
hU₂ : U₂ ∈ 𝓝 1.2
h : U₁ ×ˢ U₂ ⊆ U
⊢ ∃ V W, ↑V ×ˢ ↑W ⊆ U
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.negY ![W'.dblZ P ^ 2, W'.dblZ P ^ 3, 0] = -W'.dblZ P ^ 3

Tactic:
negY_of_Z_eq_zero rfl

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ -![W'.dblZ P ^ 2, W'.dblZ P ^ 3, 0] y = -W'.dblZ P ^ 3
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ (x₀ : A) {U : Set A}, U ∈ {U | ∃ i, U = ↑(B i)} → ∃ V ∈ {U | ∃ i, U = ↑(B i)}, V ⊆ (fun x ↦ x * x₀) ⁻¹' U

Tactic:
rintro x₀ _ ⟨i, rfl⟩
    obtain ⟨k, hk⟩ := hB.rightMul x₀ i
    use B k
    constructor
    · use k
    · exact hk

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y : R
h : x <ᵥ y
⊢ y ≠ 0

Tactic:
rintro rfl; exact not_vlt_zero _ h

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
P : W.Point
⊢ -P + P = 0

Tactic:
classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_neg, neg_add_cancel, toAffineLift_zero]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ (uniformity R).HasBasis (fun x ↦ True) fun γ ↦ {p | v.restrict (p.2 - p.1) < ↑γ}

Tactic:
convert! v.subgroups_basis.hasBasis_nhds_zero.comap _

Goal state after:
case e'_5
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x✝ : (ofClass v).ValueGroup₀ˣ
⊢ {p | v.restrict (p.2 - p.1) < ↑x✝} = (fun p ↦ p.2 + -p.1) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) x✝))
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y : R
t s : ↥(posSubmonoid R)
⊢ ¬ValueGroupWithZero.mk y s ≤ ValueGroupWithZero.mk x t ↔ x * ↑s <ᵥ y * ↑t

Tactic:
← not_vle,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y : R
t s : ↥(posSubmonoid R)
⊢ ¬ValueGroupWithZero.mk y s ≤ ValueGroupWithZero.mk x t ↔ ¬y * ↑t ≤ᵥ x * ↑s
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst✝² : IsUniformAddGroup R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
⊢ (𝓤 R).HasBasis (fun x ↦ True) fun γ ↦ {p | v.restrict (p.2 - p.1) < ↑γ}

Tactic:
convert! v.subgroups_basis.hasBasis_nhds_zero.comap _

Goal state after:
case e'_5
R : Type u_1
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst✝² : IsUniformAddGroup R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
x✝ : (ofClass v).ValueGroup₀ˣ
⊢ {p | v.restrict (p.2 - p.1) < ↑x✝} = (fun p ↦ p.2 + -p.1) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) x✝))
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
u : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this : IsUniformAddGroup R := isUniformAddGroup_of_addCommGroup
⊢ _t = ⋯.topology

Tactic:
exact congrArg (fun u ↦ @UniformSpace.toTopologicalSpace R u) v.toUniformSpace_eq

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

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

Tactic:
← not_vle,

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : ValuativeRel A
inst✝² : ValuativeRel B
inst✝¹ : Algebra A B
inst✝ : ValuativeExtension A B
a b : A
⊢ ¬(algebraMap A B) b ≤ᵥ (algebraMap A B) a ↔ a <ᵥ b
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝¹ : Ring A
v : Valuation A Γ
inst✝ : v.IsRankOneDiscrete
⊢ ∃ x, v x ≠ 0 ∧ v x ≠ 1

Tactic:
by_contra! h1

Goal state after:
Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝¹ : Ring A
v : Valuation A Γ
inst✝ : v.IsRankOneDiscrete
h1 : ∀ (x : A), v x ≠ 0 → v x = 1
⊢ False
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case hH
A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n : (WithZero (Multiplicative ℤ))ˣ
hπ✝ : (exp 1)⁻¹ ∈ range ⇑v
x✝ : ∃ k, Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n
k : ℤ
h : Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n
π : A
hπ : v π = (exp 1)⁻¹
⊢ ∃ a,
    ¬(MonoidWithZeroHom.ofClass v) a = 0 ∧
      ∃ x, (MonoidWithZeroHom.ofClass v) a * ↑(Units.mk0 (exp 1)⁻¹ ⋯ ^ k) = (MonoidWithZeroHom.ofClass v) x

Tactic:
cases k with
    | ofNat n => refine ⟨1, ?_, π ^ n, ?_⟩ <;> simp [hπ]
    | negSucc n => refine ⟨π ^ (n + 1), ?_, 1, ?_⟩ <;> simp [hπ, Int.negSucc_eq, mul_assoc]

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

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
⊢ W.addY P Q = addU P Q ^ 3

Tactic:
by
  rw [addU, ← neg_div, div_pow, ← addY_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]

Goal state after:
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 : Fin 3 → R
⊢ (W'.map f).dblZ (⇑f ∘ P) = f (W'.dblZ P)

Tactic:
by
  simp only [dblZ, negY]
  map_simp

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

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Jacobian R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).negDblY (⇑↑f ∘ P) = ↑f ((W'⁄A).negDblY P)

Tactic:
← map_negDblY,

Goal state after:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Jacobian R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).negDblY (⇑↑f ∘ P) = ((W'⁄A).map ↑f).negDblY (⇑↑f ∘ P)
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case refine_1
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝ : K
h : x✝ ∈ Subring.map (algebraMap A K) ⊤
⊢ x✝ ∈ (valuation K (maximalIdeal A)).valuationSubring.toSubring

Tactic:
obtain ⟨_, _, rfl⟩ := Subring.mem_map.mp h

Goal state after:
case refine_1
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
w✝ : A
left✝ : w✝ ∈ ⊤
h : (algebraMap A K) w✝ ∈ Subring.map (algebraMap A K) ⊤
⊢ (algebraMap A K) w✝ ∈ (valuation K (maximalIdeal A)).valuationSubring.toSubring
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: e : ℤ ≃+o ℤ
H : e 1 = -1
⊢ 0 < e 1

Tactic:
rw [← map_zero e, map_lt_map_iff]

Goal state after:
e : ℤ ≃+o ℤ
H : e 1 = -1
⊢ 0 < 1
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: e : ℤ ≃+o ℤᵒᵈ
H : e 1 = 1
⊢ 0 < e 1

Tactic:
rw [← map_zero e, map_lt_map_iff]

Goal state after:
e : ℤ ≃+o ℤᵒᵈ
H : e 1 = 1
⊢ 0 < 1