mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.FreeModule.Norm

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
i : ι
⊢ ((Matrix.toLin b' b') (Matrix.diagonal (smithCoeffs b (span {f}) ⋯))) (b' i) =
    (↑(Algebra.lmul R S).toRingHom f)
      ((LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
        ((b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι)) (b' i)))

Tactic:
Matrix.toLin_apply,

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
i : ι
⊢ ∑ j, (Matrix.diagonal (smithCoeffs b (span {f}) ⋯)).mulVec (⇑(b'.repr (b' i))) j • b' j =
    (↑(Algebra.lmul R S).toRingHom f)
      ((LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
        ((b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι)) (b' i)))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case e'_2.e'_6
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
⊢ span
      (⇑(mk W) ''
        {C (X - C x), Y - C (C y), Y - C (C (W.negY x y)),
          C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y}) =
    ⊤

Tactic:
← map_span

Goal state after:
case e'_2.e'_6
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
⊢ Ideal.map (mk W)
      (span
        {C (X - C x), Y - C (C y), Y - C (C (W.negY x y)),
          C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y}) =
    ⊤
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
hx :
  W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - (3 * W'.addX x₁ x₂ ℓ ^ 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) = 0 ∧
    2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) = 0
⊢ eval (W'.addX x₁ x₂ ℓ)
      (C 2 * (C ℓ * (X - C x₁) + C y₁) * (0 * (X - C x₁) + C ℓ * (1 - 0) + 0) +
          ((0 * X + C W'.a₁ * 1 + 0) * (C ℓ * (X - C x₁) + C y₁) +
            (C W'.a₁ * X + C W'.a₃) * (0 * (X - C x₁) + C ℓ * (1 - 0) + 0)) -
        (C ↑3 * X ^ (3 - 1) + (0 * X ^ 2 + C W'.a₂ * (C 2 * X * 1)) + (0 * X + C W'.a₄ * 1) + 0)) =
    0

Tactic:
simp only [zero_add, add_zero, sub_zero, zero_mul, mul_one]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
hx :
  W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - (3 * W'.addX x₁ x₂ ℓ ^ 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) = 0 ∧
    2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) = 0
⊢ eval (W'.addX x₁ x₂ ℓ)
      (C 2 * (C ℓ * (X - C x₁) + C y₁) * C ℓ + (C W'.a₁ * (C ℓ * (X - C x₁) + C y₁) + (C W'.a₁ * X + C W'.a₃) * C ℓ) -
        (C ↑3 * X ^ (3 - 1) + C W'.a₂ * (C 2 * X) + C W'.a₄)) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y ℓ : R
⊢ linePolynomial (f x) (f y) (f ℓ) = Polynomial.map f (linePolynomial x y ℓ)

Tactic:
simp only [linePolynomial]
  map_simp

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
⊢ c.π.app j ⁻¹ᵁ (D.obj j).basicOpen r ≤ c.π.app i ⁻¹ᵁ U

Tactic:
preimage_basicOpen_top

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
⊢ (((Functor.const I).obj c.pt).obj k).basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r) ≤ c.π.app i ⁻¹ᵁ U
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ C ((Algebra.norm R[X]) (p • 1 + q • (mk W') Y)) - (C p + C q * Y) * (C p + C q * (-Y - C (C W'.a₁ * X + C W'.a₃))) =
    W'.polynomial * C q ^ 2

Tactic:
by simp only [norm_smul_basis, polynomial]; C_simp; ring1

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
⊢ (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:
simp only [hp, hdq, neg_zero, zero_sub, zero_mul, zero_pow two_ne_zero, degree_neg]
    exact (max_bot_left _).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_3.refine_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)
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)
⊢ Set.range ⇑s.snd ⊆ Set.range ⇑(𝒰.f k)

Tactic:
simp only [hV'', Set.range_subset_iff, Set.mem_preimage, SetLike.mem_coe]

Goal state after:
case refine_3.refine_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)
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)
⊢ ∀ (y : ↥s.pt), (c.π.app i) (s.snd y) ∈ V k
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case zero
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
a₂✝ : W.Point
hP : toClass zero = toClass a₂✝
⊢ -zero = -a₂✝

Tactic:
← add_eq_zero,

Goal state after:
case zero
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
a₂✝ : W.Point
hP : toClass zero = toClass a₂✝
⊢ -zero + a₂✝ = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case some
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x✝ y✝ : F
h : W.Nonsingular x✝ y✝
a₂✝ : W.Point
hP : toClass (some x✝ y✝ h) = toClass a₂✝
⊢ -some x✝ y✝ h = -a₂✝

Tactic:
← add_eq_zero,

Goal state after:
case some
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x✝ y✝ : F
h : W.Nonsingular x✝ y✝
a₂✝ : W.Point
hP : toClass (some x✝ y✝ h) = toClass a₂✝
⊢ -some x✝ y✝ h + a₂✝ = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C X * (C W.preΨ₄ * W.ψ₂) ^ 2 - W.ψ (4 + 1) * W.ψ (4 - 1) =
    C X * C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 4 * C W.Ψ₃ + C W.Ψ₃ ^ 4

Tactic:
show (4 + 1 : ℤ) = 2 * 2 + 1 by rfl,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C X * (C W.preΨ₄ * W.ψ₂) ^ 2 - W.ψ (2 * 2 + 1) * W.ψ (4 - 1) =
    C X * C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 4 * C W.Ψ₃ + C W.Ψ₃ ^ 4
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.b₂ = 1 + 4 * W.a₂

Tactic:
by
  rw [b₂, a₁_of_isCharTwoJNeZeroNF]
  ring1

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

Goal state before:
pp: case pos
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
⊢ ∃ C, C • E = E'

Tactic:
have ha₆' := E'.Δ'.ne_zero

Goal state after:
case pos
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'.Δ' ≠ 0
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m :=
  fun {m n} {p} ↦ coeff_pow_of_natDegree_le
⊢ (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n)

Tactic:
induction n using normEDSRec with
  | zero => simpa only [preΨ'_zero] using ⟨natDegree_zero.le, Int.cast_zero.symm⟩
  | one => simpa only [preΨ'_one] using ⟨natDegree_one.le, coeff_one_zero.trans Int.cast_one.symm⟩
  | two => simpa only [preΨ'_two] using ⟨natDegree_one.le, coeff_one_zero.trans Int.cast_one.symm⟩
  | three => simpa only [preΨ'_three] using ⟨W.natDegree_Ψ₃_le, W.coeff_Ψ₃ ▸ Int.cast_three.symm⟩
  | four => simpa only [preΨ'_four] using ⟨W.natDegree_preΨ₄_le, W.coeff_preΨ₄ ▸ Int.cast_two.symm⟩
  | even m h₁ h₂ h₃ h₄ h₅ =>
    constructor
    · nth_rw 1 [preΨ'_even, ← max_self <| expDegree _, (expDegree_rec m).1.1, (expDegree_rec m).1.2]
      exact natDegree_sub_le_of_le (dm (dm (dp h₂.1) h₃.1) h₅.1) (dm (dm h₁.1 h₃.1) (dp h₄.1))
    · nth_rw 1 [preΨ'_even, coeff_sub, (expDegree_rec m).1.1, cm (dm (dp h₂.1) h₃.1) h₅.1,
        cm (dp h₂.1) h₃.1, cp h₂.1, h₂.2, h₃.2, h₅.2, (expDegree_rec m).1.2,
        cm (dm h₁.1 h₃.1) (dp h₄.1), cm h₁.1 h₃.1, h₁.2, cp h₄.1, h₃.2, h₄.2, (expCoeff_rec m).1]
      norm_cast
  | odd m h₁ h₂ h₃ h₄ =>
    rw [preΨ'_odd]
    constructor
    · nth_rw 1 [← max_self <| expDegree _, (expDegree_rec m).2.1, (expDegree_rec m).2.2]
      refine natDegree_sub_le_of_le (dm (dm h₄.1 (dp h₂.1)) ?_) (dm (dm h₁.1 (dp h₃.1)) ?_) <;>
        split_ifs <;> simp only [natDegree_one.le, dp W.natDegree_Ψ₂Sq_le]
    · nth_rw 1 [coeff_sub, (expDegree_rec m).2.1, cm (dm h₄.1 (dp h₂.1)), cm h₄.1 (dp h₂.1),
        h₄.2, cp h₂.1, h₂.2, apply_ite₂ coeff, cp W.natDegree_Ψ₂Sq_le, coeff_Ψ₂Sq, coeff_one_zero,
        (expDegree_rec m).2.2, cm (dm h₁.1 (dp h₃.1)), cm h₁.1 (dp h₃.1), h₁.2, cp h₃.1, h₃.2,
        apply_ite₂ coeff, cp W.natDegree_Ψ₂Sq_le, coeff_one_zero, coeff_Ψ₂Sq, (expCoeff_rec m).2]
      · norm_cast
      all_goals split_ifs <;> simp only [natDegree_one.le, dp W.natDegree_Ψ₂Sq_le]

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

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

Tactic:
rcases (nonsingular_iff _).mp hP with ⟨hP, hP'⟩
    refine (nonsingular_iff P).mpr ⟨(equation_smul P hu).mp hP, ?_⟩
    contrapose! hP'
    simp only [smul_fin3_ext]
    exact ⟨by linear_combination (norm := ring1) u ^ 4 * hP'.left,
      by linear_combination (norm := ring1) u ^ 3 * hP'.right.left,
      by linear_combination (norm := ring1) u ^ 5 * hP'.right.right⟩

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
⊢ (W.ΨSq n).coeff (n.natAbs ^ 2 - 1) = ↑n ^ 2

Tactic:
coeff_ΨSq

Goal state after:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
⊢ ↑n ^ 2 = ↑n ^ 2
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:
by
  simp only [dblU_eq, smul_fin3_ext]
  ring1

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

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
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
⊢ (W'⁄B).polynomial = (MvPolynomial.map ↑f) (W'⁄A).polynomial

Tactic:
by
  rw [← map_polynomial, map_baseChange]

Goal state after:
Module: Mathlib.Data.Int.WithZero

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

Tactic:
dif_neg hx,

Goal state after:
case neg
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
hx : x ≠ 0
hy : y ≠ 0
⊢ e ^ toAdd (unzero hxy) = e ^ toAdd (unzero hx) * if hx : y = 0 then 0 else e ^ toAdd (unzero hx)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
⊢ ¬(P x / P z ^ 2 = Q x / Q z ^ 2 ∧ P y / P z ^ 3 = W.toAffine.negY (Q x / Q z ^ 2) (Q y / Q z ^ 3))

Tactic:
rwa [← X_eq_iff hPz hQz, ← Y_eq_iff' hPz hQz]

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
⊢ W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) =
    (P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z * addZ P Q)

Tactic:
rw [Affine.slope_of_X_ne <| by rwa [ne_eq, ← X_eq_iff hPz hQz],
    div_sub_div _ _ (pow_ne_zero 2 hPz) (pow_ne_zero 2 hQz), mul_comm <| _ ^ 2, addZ]

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 * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ (P y / P z ^ 3 - Q y / Q z ^ 3) / ((P x * Q z ^ 2 - Q x * P z ^ 2) / (P z ^ 2 * Q z ^ 2)) =
    (P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z * (P x * Q z ^ 2 - Q x * P z ^ 2))
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:

Tactic:
x * y < γ / y * y := mul_lt_mul_of_pos_right hx (zero_lt_iff.2 hy)
      _ = γ := div_mul_cancel₀ _ hy

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x : R
s : Set R
x✝ : ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s
r : (ofClass v).ValueGroup₀ˣ
hr : {z | v.restrict (z - x) < ↑r} ⊆ s
⊢ {a | (valuation R) (a - x) < ↑((Units.mapEquiv ↑(orderMonoidIso v).symm) r)} ⊆ s

Tactic:
convert! hr

Goal state after:
R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x : R
s : Set R
x✝¹ : ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s
r : (ofClass v).ValueGroup₀ˣ
hr : {z | v.restrict (z - x) < ↑r} ⊆ s
x✝ : R
⊢ (valuation R) (x✝ - x) < ↑((Units.mapEquiv ↑(orderMonoidIso v).symm) r) ↔ v.restrict (x✝ - x) < ↑r
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x : R
s : Set R
x✝ : ∃ γ, {a | (valuation R) (a - x) < ↑γ} ⊆ s
r : (ValueGroupWithZero R)ˣ
hr : {a | (valuation R) (a - x) < ↑r} ⊆ s
⊢ {z | v.restrict (z - x) < ↑((Units.mapEquiv ↑(orderMonoidIso v)) r)} ⊆ s

Tactic:
convert! hr

Goal state after:
R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x : R
s : Set R
x✝¹ : ∃ γ, {a | (valuation R) (a - x) < ↑γ} ⊆ s
r : (ValueGroupWithZero R)ˣ
hr : {a | (valuation R) (a - x) < ↑r} ⊆ s
x✝ : R
⊢ v.restrict (x✝ - x) < ↑((Units.mapEquiv ↑(orderMonoidIso v)) r) ↔ (valuation R) (x✝ - x) < ↑r
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
γ : (ofClass v).ValueGroup₀ˣ
h : ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v (y - x) < embedding ↑γ
⊢ ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))

Tactic:
exact h γ

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ 1 ∉ supp R

Tactic:
exact not_vle_one_zero

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case mpr
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
F : Filter R
γ : (ofClass v).ValueGroup₀ˣ
h : ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v (y - x) < embedding ↑γ
⊢ ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))

Tactic:
exact h γ

Goal state after:
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
⊢ zpowers (generator' v) = ⊤

Tactic:
rw [← map_subtype_inj, MonoidHom.map_zpowers,
    subtype_apply, ← MonoidHom.range_eq_map, Subgroup.subtype_range]

Goal state after:
Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝¹ : Ring A
v : Valuation A Γ
inst✝ : v.IsRankOneDiscrete
⊢ zpowers ↑(generator' v) = (MonoidWithZeroHom.ofClass v).valueGroup
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝¹ : Field K
v : Valuation K Γ
inst✝ : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : maximalIdeal ↥v.valuationSubring = span {r}
⊢ v.IsUniformizer ↑r

Tactic:
have hr₀ : r ≠ 0 := by
    intro h
    rw [h, Set.singleton_zero, span_zero] at hr
    exact Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal v.valuationSubring)
      (valuationSubring_not_isField v) hr
  obtain ⟨π, hπ⟩ := exists_isUniformizer_of_isCyclic_of_nontrivial v
  obtain ⟨n, u, hu⟩ := exists_pow_Uniformizer hr₀ ⟨π, hπ⟩
  rw [Uniformizer.is_generator ⟨π, hπ⟩, span_singleton_eq_span_singleton] at hr
  exact hπ.of_associated hr

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

Goal state before:
pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
I : Ideal ↥v.valuationSubring
this : ∀ (P : Ideal ↥v.valuationSubring), P.IsPrime → Submodule.IsPrincipal P
⊢ Submodule.IsPrincipal I

Tactic:
by
    exact (IsPrincipalIdealRing.of_prime this).principal I

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

Goal state before:
pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
I : Ideal ↥v.valuationSubring
⊢ ∀ (P : Ideal ↥v.valuationSubring), P.IsPrime → Submodule.IsPrincipal P

Tactic:
intro P

Goal state after:
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
I P : Ideal ↥v.valuationSubring
⊢ P.IsPrime → Submodule.IsPrincipal P