mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.221} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.221} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a b : J
f : a ⟶ b
i : (𝒱 a).I₀
⊢ (𝒱 a).f i ≫
      (D.map f ≫
          {
            toCommaMorphism :=
              (𝒱 b).glueMorphismsOverOfLocallyDirected
                (fun i ↦ ((d.cocone i).ι.app b).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯,
            prop_hom_left := trivial, prop_hom_right := trivial }).left =
    (𝒱 a).f i ≫
      ({
            toCommaMorphism :=
              (𝒱 a).glueMorphismsOverOfLocallyDirected
                (fun i ↦ ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯,
            prop_hom_left := trivial, prop_hom_right := trivial } ≫
          ((Functor.const J).obj d.glued).map f).left

Tactic:
have : (𝒱 a).f i ≫ (D.map f).left =
        ((D ⋙ Over.pullback _ _ (𝒰.f i)).map f).left ≫ (𝒱 b).f i := by
      simp [𝒱]

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.266} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.266} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a b : J
f : a ⟶ b
i : (𝒱 a).I₀
this : (𝒱 a).f i ≫ (D.map f).left = ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).map f).left ≫ (𝒱 b).f i
⊢ (𝒱 a).f i ≫
      (D.map f ≫
          {
            toCommaMorphism :=
              (𝒱 b).glueMorphismsOverOfLocallyDirected
                (fun i ↦ ((d.cocone i).ι.app b).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯,
            prop_hom_left := trivial, prop_hom_right := trivial }).left =
    (𝒱 a).f i ≫
      ({
            toCommaMorphism :=
              (𝒱 a).glueMorphismsOverOfLocallyDirected
                (fun i ↦ ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯,
            prop_hom_left := trivial, prop_hom_right := trivial } ≫
          ((Functor.const J).obj d.glued).map f).left
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

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

Tactic:
linear_combination -W.c_relation + 576 * W.Δ * CharP.cast_eq_zero R 3

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

Goal state before:
pp: case a
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ 4 = 0

pp: case c
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ 2 * W.b₄ = 0

Tactic:
· linear_combination 2 * CharP.cast_eq_zero R 2

Goal state after:
case c
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ 2 * W.b₄ = 0
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).polynomialY = Polynomial.map (mapRingHom f) W.polynomialY

Tactic:
simp only [polynomialY]
  map_simp

Goal state after:
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₂ = 0

Tactic:
by
  rw [slope, if_pos hx, if_pos hy]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (C • W).c₄ = ↑C.u⁻¹ ^ 4 * W.c₄

Tactic:
simp only [c₄, variableChange_b₂, variableChange_b₄]

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)) ^ 2 - 24 * (↑C.u⁻¹ ^ 4 * (W.b₄ + C.r * W.b₂ + 6 * C.r ^ 2)) =
    ↑C.u⁻¹ ^ 4 * (W.b₂ ^ 2 - 24 * W.b₄)
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)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this : CompactSpace ↥c.pt
i : ↥c.pt → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ U x
t : (x : ↥c.pt) → ↑Γ(D.obj (i x), U x)
ht : ∀ (x : ↥c.pt), (ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i x)) (U x))) (t x) = (s |_ c.π.app (i x) ⁻¹ᵁ U x) ⋯
j : ↥c.pt → ↥c.pt → I
fjx : (x y : ↥c.pt) → j x y ⟶ i x
fjy : (x y : ↥c.pt) → j x y ⟶ i y
hj :
  ∀ (x y : ↥c.pt),
    ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fjx x y)) (U x))) (t x) |_
          (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y))
        ⋯ =
      ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fjy x y)) (U y))) (t y) |_
          (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y))
        ⋯
σ : Finset ↥c.pt
hσ : ⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ U 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)) ⁻¹ᵁ U (σi x)).carrier
S : Finset I := Finset.image i σ ∪ Finset.image₂ j σ σ
hiS : ∀ {x : ↥c.pt}, x ∈ σ → i x ∈ S
⊢ ∃ i t, s = (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) t

Tactic:
have hjS {x y} (hx : x ∈ σ) (hy : y ∈ σ) : j x y ∈ S :=
    Finset.subset_union_right (Finset.mem_image₂_of_mem hx hy)

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)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this : CompactSpace ↥c.pt
i : ↥c.pt → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ U x
t : (x : ↥c.pt) → ↑Γ(D.obj (i x), U x)
ht : ∀ (x : ↥c.pt), (ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i x)) (U x))) (t x) = (s |_ c.π.app (i x) ⁻¹ᵁ U x) ⋯
j : ↥c.pt → ↥c.pt → I
fjx : (x y : ↥c.pt) → j x y ⟶ i x
fjy : (x y : ↥c.pt) → j x y ⟶ i y
hj :
  ∀ (x y : ↥c.pt),
    ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fjx x y)) (U x))) (t x) |_
          (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y))
        ⋯ =
      ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fjy x y)) (U y))) (t y) |_
          (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y))
        ⋯
σ : Finset ↥c.pt
hσ : ⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ U 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)) ⁻¹ᵁ U (σi x)).carrier
S : Finset I := Finset.image i σ ∪ Finset.image₂ j σ σ
hiS : ∀ {x : ↥c.pt}, x ∈ σ → i x ∈ S
hjS : ∀ {x y : ↥c.pt}, x ∈ σ → y ∈ σ → j x y ∈ S
⊢ ∃ i t, s = (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) t
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
p q r s : ℤ
⊢ atomRel W (-(2 * p + s)) (-(2 * q + s)) (-(2 * r + s)) (-s) = atomRel W (2 * p + s) (2 * q + s) (2 * r + s) s

Tactic:
atomRel_neg₁ odd,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
p q r s : ℤ
⊢ atomRel W (2 * p + s) (-(2 * q + s)) (-(2 * r + s)) (-s) = atomRel W (2 * p + s) (2 * q + s) (2 * r + s) s
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
F : Type u
K : Type v
L : Type w
inst✝¹³ : CommRing R
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
W' : Affine R
inst✝⁹ : DecidableEq F
inst✝⁸ : DecidableEq K
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : Algebra F K
inst✝² : IsScalarTower R F K
inst✝¹ : Algebra F L
inst✝ : IsScalarTower R F L
f : K →ₐ[F] L
P : (W'⁄F).Point
this : Subsingleton (F →ₐ[F] L)
⊢ (map f) ((baseChange F K) P) = (baseChange F L) P

Tactic:
convert! map_map (Algebra.ofId F K) f P

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

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

Tactic:
rcases n.even_or_odd' with ⟨n, rfl | rfl⟩
  · 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
  · push_cast [expDegree, show (2 * n + 1) ^ 2 = 2 * (2 * n * (n + 1)) + 1 by ring1,
      n.not_even_two_mul_add_one, Nat.add_sub_cancel, Nat.mul_div_cancel_left _ two_pos]
    ring1

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

Goal state before:
pp: F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP F 2
⊢ W.c₄ ^ 3 / W.Δ = 1 / W.a₆

Tactic:
c₄_of_isCharTwoJNeZeroNF_of_char_two,

Goal state after:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP F 2
⊢ 1 ^ 3 / W.Δ = 1 / W.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
P : Fin 3 → R
n : Fin (Nat.succ 0).succ.succ
⊢ ![P x, P y, P z] n = P n

Tactic:
fin_cases n <;> rfl

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

Goal state before:
pp: R : Type r
F : Type u
inst✝⁵ : CommRing R
inst✝⁴ : Field F
W' : Jacobian R
W : Jacobian F
S : Type s
inst✝³ : CommRing S
A : Type u
inst✝² : CommRing A
B : Type v
inst✝¹ : CommRing B
K : Type v
inst✝ : Field K
x✝² x✝¹ : R
x✝ : Fin 3 → R
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
by simp only [smul_fin3, mul_pow, mul_assoc, fin3_def_ext]

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

Goal state before:
pp: case of_j_eq_zero.of_j_eq_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 2
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (C • E).IsCharTwoJEqZeroNF
C' : VariableChange F
inst✝ : (C' • E').IsCharTwoJEqZeroNF
⊢ ∃ C, C • E = E'

Tactic:
obtain ⟨C'', hC⟩ := exists_variableChange_of_char_two_of_j_eq_zero (C • E) (C' • E')

Goal state after:
case of_j_eq_zero.of_j_eq_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 2
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (C • E).IsCharTwoJEqZeroNF
C' : VariableChange F
inst✝ : (C' • E').IsCharTwoJEqZeroNF
C'' : VariableChange F
hC : C'' • C • E = C' • E'
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n)

Tactic:
by
  let dm {m n p q} : _ → _ → (p * q : R[X]).natDegree ≤ m + n := natDegree_mul_le_of_le
  let dp {m n p} : _ → (p ^ n : R[X]).natDegree ≤ n * m := natDegree_pow_le_of_le n
  let cm {m n p q} : _ → _ → (p * q : R[X]).coeff (m + n) = _ := coeff_mul_add_eq_of_natDegree_le
  let cp {m n p} : _ → (p ^ m : R[X]).coeff (m * n) = _ := coeff_pow_of_natDegree_le
  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.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
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
⊢ (W.Φ ↑n).natDegree ≤ n ^ 2 ∧ (W.Φ ↑n).coeff (n ^ 2) = 1

Tactic:
rcases n with _ | _ | n

Goal state after:
case zero
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
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
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
⊢ (W.Φ ↑0).natDegree ≤ 0 ^ 2 ∧ (W.Φ ↑0).coeff (0 ^ 2) = 1

case succ.zero
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
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
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
⊢ (W.Φ ↑(0 + 1)).natDegree ≤ (0 + 1) ^ 2 ∧ (W.Φ ↑(0 + 1)).coeff ((0 + 1) ^ 2) = 1

case succ.succ
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
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
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
⊢ (W.Φ ↑(n + 1 + 1)).natDegree ≤ (n + 1 + 1) ^ 2 ∧ (W.Φ ↑(n + 1 + 1)).coeff ((n + 1 + 1) ^ 2) = 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
⊢ P x ≠ 0

Tactic:
intro hPx
  simp only [nonsingular_of_Z_eq_zero hPz, equation_of_Z_eq_zero hPz, hPx, mul_zero, zero_mul,
    zero_pow <| OfNat.ofNat_ne_zero _, ne_self_iff_false, or_false, false_or] at hP
  rwa [pow_eq_zero_iff two_ne_zero, hP.left, eq_self, true_and, mul_zero, ne_self_iff_false] at hP

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

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.negY P / P z ^ 3 + (-W.a₁ * P x / P z ^ 2 * 1 + W.a₃ * (P z ^ 3 / P z ^ 3)) -
      (W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3) + (-W.a₁ * P x / P z ^ 2 * (P z / P z) + W.a₃ * 1)) =
    0

Tactic:
rw [negY, Affine.negY]; 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'.negDblY (u • P) = (u ^ 4) ^ 3 * W'.negDblY P

Tactic:
simp only [negDblY, dblU_smul, dblX_smul, negY_smul, smul_fin3_ext]
  ring1

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

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (u • P) = toAffine W P

Tactic:
rw [toAffine_of_Z_ne_zero ((nonsingular_smul P hu).mpr hP) <| mul_ne_zero hu.ne_zero hPz,
        toAffine_of_Z_ne_zero hP hPz, Affine.Point.some.injEq]

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ (u • P) x / (u • P) z ^ 2 = P x / P z ^ 2 ∧ (u • P) y / (u • P) z ^ 3 = P y / P z ^ 3
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
b c : ValueGroupWithZero R
hbc : b ≤ c
a₁ : R
a₂ : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk a₁ a₂ ≤ b
⊢ ValueGroupWithZero.mk a₁ a₂ ≤ c

Tactic:
induction b using ValueGroupWithZero.ind with

Goal state after:
case mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
c : ValueGroupWithZero R
a₁ : R
a₂ : ↥(posSubmonoid R)
b₁ : R
b₂ : ↥(posSubmonoid R)
hbc : ValueGroupWithZero.mk b₁ b₂ ≤ c
hab : ValueGroupWithZero.mk a₁ a₂ ≤ ValueGroupWithZero.mk b₁ b₂
⊢ ValueGroupWithZero.mk a₁ a₂ ≤ c
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ Nontrivial (ValueGroupWithZero R)ˣ → IsNontrivial R

Tactic:
· rintro ⟨r, s, h⟩
    rcases eq_or_ne r 1 with rfl | hr
    · exact ⟨s.val, by simp, by simpa using h.symm⟩
    · exact ⟨r.val, by simp, by simpa using hr⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹⁴ : Ring α
inst✝¹³ : UniformSpace α
inst✝¹² : IsTopologicalRing α
inst✝¹¹ : IsUniformAddGroup α
β : Type u
inst✝¹⁰ : UniformSpace β
inst✝⁹ : Ring β
inst✝⁸ : IsUniformAddGroup β
inst✝⁷ : IsTopologicalRing β
f : α →+* β
hf : Continuous ⇑f
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : IsUniformAddGroup A
inst✝³ : IsTopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion A
a : A
⊢ (coeRingHom.comp (algebraMap R A)) r * ↑a = ↑a * (coeRingHom.comp (algebraMap R A)) r

Tactic:
by
      simpa only [coe_mul] using! congr_arg ((↑) : A → Completion A) (Algebra.commutes r a)

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
a b : R
hab : a * b ∈ I
ha : a ∉ I
hb : b ∉ I
⊢ False

Tactic:
have h₁ : P (I ⊔ span {a}) := of_not_not <| hI.not_prop_of_gt (Submodule.lt_sup_iff_notMem.2 ha)

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
I : Ideal R
hI : Maximal (fun x ↦ ¬P x) I
a b : R
hab : a * b ∈ I
ha : a ∉ I
hb : b ∉ I
h₁ : P (I ⊔ span {a})
⊢ False
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case h
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer ↑π₁
h2 : v.IsUniformizer ↑π₂
hval : v ((↑π₁)⁻¹ * ↑π₂) = 1
p : ↥v.integer := ⟨(↑π₁)⁻¹ * ↑π₂, ⋯⟩
hp : p = ⟨(↑π₁)⁻¹ * ↑π₂, ⋯⟩
⊢ ↑(π₁ * ↑⋯.unit) = ↑π₂

Tactic:
simp [hp, ← mul_assoc, mul_inv_cancel₀ h1.ne_zero]

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 Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := ⋯
hvr_def : vr = Units.mk0 (v ↑r) hr₀
⊢ ↑vr ∈ range ⇑(MonoidWithZeroHom.ofClass v)

Tactic:
hvr_def,

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
⊢ ↑(Units.mk0 (v ↑r) hr₀) ∈ range ⇑(MonoidWithZeroHom.ofClass v)
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 Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
hm₀ : 0 ≤ m
n : ℕ
hn : m = ↑n
hpow : v (↑π.val ^ (-m) * ↑r) = 1
a : ↥v.valuationSubring := ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha : a = ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
⊢ ¬↑π.val ^ m = 0

Tactic:
rw [hn, zpow_natCast, pow_eq_zero_iff', not_and_or]

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
hm₀ : 0 ≤ m
n : ℕ
hn : m = ↑n
hpow : v (↑π.val ^ (-m) * ↑r) = 1
a : ↥v.valuationSubring := ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha : a = ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
⊢ ¬↑π.val = 0 ∨ ¬n ≠ 0
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y r s : K
y_ne : y ≠ 0
hr : r ≠ 0
hs : s ≠ 0
h : v (x - y) < min (v s / v r * (v y * v y)) (v y)
⊢ v (x⁻¹ - y⁻¹) * v r < v s

Tactic:
have hr' : 0 < v r := by simp [zero_lt_iff, hr]
  let γ : Γ₀ˣ := .mk0 (v s / v r) (by simp [hs, hr])
  calc
    v (x⁻¹ - y⁻¹) * v r < γ * v r := by gcongr; exact Valuation.inversion_estimate v y_ne h
    _ = v s := div_mul_cancel₀ _ (by simpa)

Goal state after: