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

Goal state before:
pp: case hP₄
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
⊢ ∀ (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        (∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (Away c)],
            Statement R₀ (Away c) n
              { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val }) →
          (∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (R ⧸ Ideal.span {c})],
              Statement R₀ (R ⧸ Ideal.span {c}) n
                { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val }) →
            ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n e

Tactic:
c

Goal state after:
case hP₄
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
c : R
⊢ ∀ (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        (∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (Away c)],
            Statement R₀ (Away c) n
              { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val }) →
          (∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (R ⧸ Ideal.span {c})],
              Statement R₀ (R ⧸ Ideal.span {c}) n
                { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val }) →
            ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n e
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.twoTorsionPolynomial.discr = 16 * W.Δ

Tactic:
simp only [b₂, b₄, b₆, b₈, Δ, twoTorsionPolynomial, Cubic.discr]

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (W.a₁ ^ 2 + 4 * W.a₂) ^ 2 * (2 * (2 * W.a₄ + W.a₁ * W.a₃)) ^ 2 - 4 * 4 * (2 * (2 * W.a₄ + W.a₁ * W.a₃)) ^ 3 -
          4 * (W.a₁ ^ 2 + 4 * W.a₂) ^ 3 * (W.a₃ ^ 2 + 4 * W.a₆) -
        27 * 4 ^ 2 * (W.a₃ ^ 2 + 4 * W.a₆) ^ 2 +
      18 * 4 * (W.a₁ ^ 2 + 4 * W.a₂) * (2 * (2 * W.a₄ + W.a₁ * W.a₃)) * (W.a₃ ^ 2 + 4 * W.a₆) =
    16 *
      (-(W.a₁ ^ 2 + 4 * W.a₂) ^ 2 *
              (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2) -
            8 * (2 * W.a₄ + W.a₁ * W.a₃) ^ 3 -
          27 * (W.a₃ ^ 2 + 4 * W.a₆) ^ 2 +
        9 * (W.a₁ ^ 2 + 4 * W.a₂) * (2 * W.a₄ + W.a₁ * W.a₃) * (W.a₃ ^ 2 + 4 * W.a₆))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : CharP R 3
⊢ W.j = 0 ↔ W.b₂ ^ 6 = 0

Tactic:
rw [j_of_char_three, Units.mul_right_eq_zero]

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : Nontrivial R
⊢ W.polynomial ≠ 0

Tactic:
rw [polynomial_eq]

Goal state after:
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : Nontrivial R
⊢ { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly,
        d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly }.toPoly ≠
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : Nontrivial R
⊢ W.polynomial.degree = 2

Tactic:
rw [polynomial_eq]

Goal state after:
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : Nontrivial R
⊢ { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly,
          d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly }.toPoly.degree =
    2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : Nontrivial R
⊢ W.polynomial.natDegree = 2

Tactic:
rw [polynomial_eq]

Goal state after:
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : Nontrivial R
⊢ { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly,
          d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly }.toPoly.natDegree =
    2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
hpq : p • 1 + q • (mk W') Y = 0
h : ∑ i, ![p, q] i • (CoordinateRing.basis W') i = 0 → ∀ (i : Fin 2), ![p, q] i = 0
⊢ p = 0 ∧ q = 0

Tactic:
rw [Fin.sum_univ_succ, basis_zero, Fin.sum_univ_one, Fin.succ_zero_eq_one, basis_one] at h

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
hpq : p • 1 + q • (mk W') Y = 0
h : ![p, q] 0 • 1 + ![p, q] 1 • (mk W') Y = 0 → ∀ (i : Fin 2), ![p, q] i = 0
⊢ p = 0 ∧ q = 0
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hC
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))
x✝ : R
⊢ ((g.comp σ).comp MvPolynomial.C) x✝ = ((RingHom.id (MvPolynomial (Fin m) R)).comp MvPolynomial.C) x✝

Tactic:
simp [g, σ]

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

Goal state before:
pp: case hX
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))
i✝ : Fin m
m✝ : Fin m →₀ ℕ
⊢ MvPolynomial.coeff m✝ ((g.comp σ) (MvPolynomial.X i✝)) =
    MvPolynomial.coeff m✝ ((RingHom.id (MvPolynomial (Fin m) R)) (MvPolynomial.X i✝))

Tactic:
simp [g, σ]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
← neg_atom odd c d,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atom W a b * atom W c d = -atom W a b * -atom W c d
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := (y₁ - W.negY x₁ y₁) ^ 2
hxy : (y₁ - W.negY x₁ y₁) ^ 2 ≠ 0
⊢ C (C y⁻¹) * (Y - W.negPolynomial) * (Y - W.negPolynomial) =
    1 + C (C (y⁻¹ * 4)) * (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) +
        C (C y⁻¹ * (C 4 * X ^ 2 + C (4 * x₁ + b₂ W) * X + C (4 * x₁ ^ 2 + b₂ W * x₁ + 2 * b₄ W))) * C (X - C x₁) +
      0 * C (X - C x₁)

Tactic:
negPolynomial,

Goal state after:
case pos
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := (y₁ - W.negY x₁ y₁) ^ 2
hxy : (y₁ - W.negY x₁ y₁) ^ 2 ≠ 0
⊢ C (C y⁻¹) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) =
    1 + C (C (y⁻¹ * 4)) * (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) +
        C (C y⁻¹ * (C 4 * X ^ 2 + C (4 * x₁ + b₂ W) * X + C (4 * x₁ ^ 2 + b₂ W * x₁ + 2 * b₄ W))) * C (X - C x₁) +
      0 * C (X - C x₁)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℤ
⊢ normEDS b c d (2 * m + 1) =
    normEDS b c d (m + 2) * normEDS b c d m ^ 3 - normEDS b c d (m - 1) * normEDS b c d (m + 1) ^ 3

Tactic:
simp_rw [normEDS, preNormEDS_odd, if_neg m.not_even_two_mul_add_one, Int.even_add, Int.even_sub,
    even_two, iff_true, Int.not_even_one, iff_false]

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℤ
⊢ ((preNormEDS (b ^ 4) c d (m + 2) * preNormEDS (b ^ 4) c d m ^ 3 * if Even m then b ^ 4 else 1) -
        preNormEDS (b ^ 4) c d (m - 1) * preNormEDS (b ^ 4) c d (m + 1) ^ 3 * if Even m then 1 else b ^ 4) *
      1 =
    (preNormEDS (b ^ 4) c d (m + 2) * if Even m then b else 1) *
        (preNormEDS (b ^ 4) c d m * if Even m then b else 1) ^ 3 -
      (preNormEDS (b ^ 4) c d (m - 1) * if ¬Even m then b else 1) *
        (preNormEDS (b ^ 4) c d (m + 1) * if ¬Even m then b else 1) ^ 3
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
k : ℤ
P : ℕ → Sort u_4
zero : P 0
one : P 1
even : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 1) → P k) → P (2 * (m + 1))
odd : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 1) + 1 → P k) → P (2 * (m + 1) + 1)
n : ℕ
h : (k : ℕ) → k < 2 * 0 → P k
⊢ P (2 * 0)

pp: case succ
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
k : ℤ
P : ℕ → Sort u_4
zero : P 0
one : P 1
even : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 1) → P k) → P (2 * (m + 1))
odd : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 1) + 1 → P k) → P (2 * (m + 1) + 1)
n n✝ : ℕ
h : (k : ℕ) → k < 2 * (n✝ + 1) → P k
⊢ P (2 * (n✝ + 1))

Tactic:
exacts [zero, even _ h]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (X * W.ΨSq (↑n + 1) - W.preΨ (↑n + 1 + 1) * W.preΨ (↑n + 1 - 1) * if Even (↑n + 1) then 1 else W.Ψ₂Sq) =
    (X * W.preΨ' (n + 1) ^ 2 * if Even n then 1 else W.Ψ₂Sq) -
      W.preΨ' (n + 2) * W.preΨ' n * if Even n then W.Ψ₂Sq else 1

Tactic:
add_sub_cancel_right

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (X * W.ΨSq (↑n + 1) - W.preΨ (↑n + 1 + 1) * W.preΨ ↑n * if Even (↑n + 1) then 1 else W.Ψ₂Sq) =
    (X * W.preΨ' (n + 1) ^ 2 * if Even n then 1 else W.Ψ₂Sq) -
      W.preΨ' (n + 2) * W.preΨ' n * if Even n then W.Ψ₂Sq else 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
F : Type u_2
inst✝¹ : Field F
W : WeierstrassCurve R
inst✝ : W.IsCharThreeNF
⊢ W.IsCharNeTwoNF

Tactic:
cases ‹W.IsCharThreeNF› <;> infer_instance

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ (W.toShortNFOfCharThree • W).a₂ = W.b₂

Tactic:
simp_rw [toShortNFOfCharThree, toCharNeTwoNF, variableChange_a₂, inv_one, Units.val_one, b₂]
  linear_combination (-W.a₂ - W.a₁ ^ 2) * CharP.cast_eq_zero R 3

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ W.b₆ = 0

Tactic:
rw [b₆_of_isCharTwoJNeZeroNF]

Goal state after:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ 4 * W.a₆ = 0
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
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.c₄ ^ 3 / ↑E.Δ' = E'.c₄ ^ 3 / ↑E'.Δ'
⊢ ∃ C, C • E = E'

Tactic:
div_eq_div_iff E.Δ'.ne_zero E'.Δ'.ne_zero,

Goal state after:
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.c₄ ^ 3 * ↑E'.Δ' = E'.c₄ ^ 3 * ↑E.Δ'
⊢ ∃ C, C • E = E'
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
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 = 0 ∨ E.a₆ ^ 2 = 0
ha₄ : E.a₄ = 0
ha₆ : E.a₆ ≠ 0
⊢ E'.a₄ = 0

Tactic:
exact (pow_eq_zero_iff three_ne_zero).1 <| heq.resolve_right <| pow_ne_zero 2 ha₆

Goal state after:
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✝⁴ : 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
k : I
fki : k ⟶ i
ak : (j : ↥s) → ↑(D.map fki ⁻¹ᵁ 𝒱 j) ⟶ X
hak : ∀ (j : ↥s), ak j ≫ f = (D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ t.app k
hak' : ∀ (j : ↥s), c.π.app k ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j = (c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ a
𝒱' : ↥s → (D.obj k).Opens := fun x ↦ D.map fki ⁻¹ᵁ 𝒱 x
l : ↥s → ↥s → I
flk : (j₁ j₂ : ↥s) → l j₁ j₂ ⟶ k
hflk :
  ∀ (j₁ j₂ : ↥s),
    (D.obj (l j₁ j₂)).homOfLE ⋯ ≫ D.map (flk j₁ j₂) ∣_ D.map fki ⁻¹ᵁ 𝒱 j₁ ≫ ak j₁ =
      (D.obj (l j₁ j₂)).homOfLE ⋯ ≫ D.map (flk j₁ j₂) ∣_ D.map fki ⁻¹ᵁ 𝒱 j₂ ≫ ak j₂
l' : I
fl'k : l' ⟶ k
fl'l : (x : ↥s × ↥s) → l' ⟶ l x.1 x.2
hl' : ∀ (x : ↥s × ↥s), fl'l x ≫ flk x.1 x.2 = fl'k
⊢ ∃ l flk,
    ∀ (j₁ j₂ : ↥s),
      (D.obj l).homOfLE ⋯ ≫ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j₁ ≫ ak j₁ =
        (D.obj l).homOfLE ⋯ ≫ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j₂ ≫ ak j₂

Tactic:
refine ⟨l', fl'k, fun j₁ j₂ ↦ ?_⟩

Goal state after:
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
k : I
fki : k ⟶ i
ak : (j : ↥s) → ↑(D.map fki ⁻¹ᵁ 𝒱 j) ⟶ X
hak : ∀ (j : ↥s), ak j ≫ f = (D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ t.app k
hak' : ∀ (j : ↥s), c.π.app k ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j = (c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ a
𝒱' : ↥s → (D.obj k).Opens := fun x ↦ D.map fki ⁻¹ᵁ 𝒱 x
l : ↥s → ↥s → I
flk : (j₁ j₂ : ↥s) → l j₁ j₂ ⟶ k
hflk :
  ∀ (j₁ j₂ : ↥s),
    (D.obj (l j₁ j₂)).homOfLE ⋯ ≫ D.map (flk j₁ j₂) ∣_ D.map fki ⁻¹ᵁ 𝒱 j₁ ≫ ak j₁ =
      (D.obj (l j₁ j₂)).homOfLE ⋯ ≫ D.map (flk j₁ j₂) ∣_ D.map fki ⁻¹ᵁ 𝒱 j₂ ≫ ak j₂
l' : I
fl'k : l' ⟶ k
fl'l : (x : ↥s × ↥s) → l' ⟶ l x.1 x.2
hl' : ∀ (x : ↥s × ↥s), fl'l x ≫ flk x.1 x.2 = fl'k
j₁ j₂ : ↥s
⊢ (D.obj l').homOfLE ⋯ ≫ D.map fl'k ∣_ D.map fki ⁻¹ᵁ 𝒱 j₁ ≫ ak j₁ =
    (D.obj l').homOfLE ⋯ ≫ D.map fl'k ∣_ D.map fki ⁻¹ᵁ 𝒱 j₂ ≫ ak j₂
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: case h.e'_3
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP : P y ^ 2 = P x ^ 3 ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ : Q y ^ 2 = Q x ^ 3 ∧ (3 * Q x ^ 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
⊢ P x * (Q x ^ 2 / Q y ^ 2) * Q x = P x

Tactic:
hQ.left,

Goal state after:
case h.e'_3
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP : P y ^ 2 = P x ^ 3 ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ : Q y ^ 2 = Q x ^ 3 ∧ (3 * Q x ^ 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
⊢ P x * (Q x ^ 2 / Q x ^ 3) * Q x = P x
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
Q : PointClass F
hP : W.Nonsingular P
hQ : W.NonsingularLift Q
hPz : P z = 0
⊢ W.addMap ⟦P⟧ Q = Q

Tactic:
by
  revert hQ
  refine Q.inductionOn (motive := fun Q => _ → W.addMap _ Q = Q) fun Q hQ => ?_
  by_cases hQz : Q z = 0
  · rw [addMap_eq, add_of_Z_eq_zero hP hQ hPz hQz,
      smul_eq _ <| (isUnit_X_of_Z_eq_zero hP hPz).pow 2, Quotient.eq]
    exact Setoid.symm <| equiv_zero_of_Z_eq_zero hQ hQz
  · rw [addMap_eq, add_of_Z_eq_zero_left hP.left hPz hQz,
      smul_eq _ <| (isUnit_X_of_Z_eq_zero hP hPz).mul <| Ne.isUnit hQz]

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

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : P y * Q z ^ 3 = Q y * P z ^ 3
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![1, 1, 0]⟧

Tactic:
rw [addMap_eq, add_of_Y_eq hPz hQz hx hy hy',
      smul_eq _ <| isUnit_dblU_of_Y_eq hP hPz hQz hx hy hy']

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

Goal state before:

Tactic:
v.restrict (r * s) = v.restrict r * v.restrict s := Valuation.map_mul _ _ _
        _ < γ₀.1 * γ₀.1 := by gcongr <;> exact zero_le
        _ ≤ γ := mod_cast h

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : w ≤ᵥ 0
hz : z ≤ᵥ 0
⊢ (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : w ≤ᵥ 0
hz : ¬z ≤ᵥ 0
⊢ (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)

pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : ¬w ≤ᵥ 0
hz : z ≤ᵥ 0
⊢ (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : ¬w ≤ᵥ 0
hz : ¬z ≤ᵥ 0
⊢ (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)

Tactic:
· refine propext ⟨fun h => vle_trans ?_ (zero_vle _), fun h => vle_trans ?_ (zero_vle _)⟩
      · apply vle_mul_cancel (s * v).prop
        grw [veq_mul_right_comm, Submonoid.coe_mul, ← mul_assoc]
        apply (mul_vle_mul_left (mul_vle_mul_left h₂ v) u).trans
        grw [veq_mul_right_comm x]
        apply (mul_vle_mul_left (mul_vle_mul_left h t) u).trans
        apply vle_trans (mul_vle_mul_left (mul_vle_mul_left (mul_vle_mul_left hz s) t) u)
        simp
      · apply vle_mul_cancel (t * u).prop
        grw [veq_mul_right_comm, Submonoid.coe_mul, ← mul_assoc]
        apply (mul_vle_mul_left (mul_vle_mul_left h₁ u) v).trans
        grw [veq_mul_right_comm y]
        apply (mul_vle_mul_left (mul_vle_mul_left h s) v).trans
        apply vle_trans (mul_vle_mul_left (mul_vle_mul_left (mul_vle_mul_left hw t) s) v)
        simp

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : w ≤ᵥ 0
hz : ¬z ≤ᵥ 0
⊢ (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)

case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : ¬w ≤ᵥ 0
hz : z ≤ᵥ 0
⊢ (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)

case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : ¬w ≤ᵥ 0
hz : ¬z ≤ᵥ 0
⊢ (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case mk.mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z x✝² : R
y✝² : ↥(posSubmonoid R)
x✝¹ : R
y✝¹ : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk x✝² y✝² ≤ ValueGroupWithZero.mk x✝¹ y✝¹
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x✝² y✝² * ValueGroupWithZero.mk x✝ y✝ ≤
    ValueGroupWithZero.mk x✝¹ y✝¹ * ValueGroupWithZero.mk x✝ y✝

Tactic:
simp only [ValueGroupWithZero.mk_mul_mk, ValueGroupWithZero.mk_le_mk, Submonoid.coe_mul]

Goal state after:
case mk.mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z x✝² : R
y✝² : ↥(posSubmonoid R)
x✝¹ : R
y✝¹ : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk x✝² y✝² ≤ ValueGroupWithZero.mk x✝¹ y✝¹
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ x✝² * x✝ * (↑y✝¹ * ↑y✝) ≤ᵥ x✝¹ * x✝ * (↑y✝² * ↑y✝)
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:
by
    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: