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

Goal state before:
pp: case pos
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 n
h : 0 = i
⊢ {j} ≤ Finset.univ.val

Tactic:
simp

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

Goal state before:
pp: case neg
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 n
h : ¬0 = i
⊢ 0 ≤ Finset.univ.val

Tactic:
simp

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

Goal state before:
pp: case left.inr
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 n
⊢ (MvPolynomial.coeff i
        (Sum.elim (⇑σ ∘ x.g) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i)))
          (Sum.inr j))).degrees ≤
    Finset.univ.val

Tactic:
· simp only [MvPolynomial.algebraMap_eq, Sum.elim_inr, MvPolynomial.coeff_sub,
            MvPolynomial.coeff_C, MvPolynomial.coeff_map, σ]
          refine degrees_sub_le.trans ?_
          simp only [degrees_C, apply_ite, degrees_zero,
            Multiset.union_zero]
          split_ifs with h
          · refine (degrees_X' _).trans ?_
            simp
          · simp

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case nat.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑0) =
    preNormEDS b c d (↑0 - 1) ^ 2 * preNormEDS b c d ↑0 * preNormEDS b c d (↑0 + 2) -
      preNormEDS b c d (↑0 - 2) * preNormEDS b c d ↑0 * preNormEDS b c d (↑0 + 1) ^ 2

pp: case nat.succ.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑(0 + 1)) =
    preNormEDS b c d (↑(0 + 1) - 1) ^ 2 * preNormEDS b c d ↑(0 + 1) * preNormEDS b c d (↑(0 + 1) + 2) -
      preNormEDS b c d (↑(0 + 1) - 2) * preNormEDS b c d ↑(0 + 1) * preNormEDS b c d (↑(0 + 1) + 1) ^ 2

pp: case nat.succ.succ.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑(0 + 1 + 1)) =
    preNormEDS b c d (↑(0 + 1 + 1) - 1) ^ 2 * preNormEDS b c d ↑(0 + 1 + 1) * preNormEDS b c d (↑(0 + 1 + 1) + 2) -
      preNormEDS b c d (↑(0 + 1 + 1) - 2) * preNormEDS b c d ↑(0 + 1 + 1) * preNormEDS b c d (↑(0 + 1 + 1) + 1) ^ 2

pp: case nat.succ.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * ↑(m + 1 + 1 + 1)) =
    preNormEDS b c d (↑(m + 1 + 1 + 1) - 1) ^ 2 * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 2) -
      preNormEDS b c d (↑(m + 1 + 1 + 1) - 2) * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 1) ^ 2

Tactic:
simp

Goal state after:
case nat.succ.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑(0 + 1)) =
    preNormEDS b c d (↑(0 + 1) - 1) ^ 2 * preNormEDS b c d ↑(0 + 1) * preNormEDS b c d (↑(0 + 1) + 2) -
      preNormEDS b c d (↑(0 + 1) - 2) * preNormEDS b c d ↑(0 + 1) * preNormEDS b c d (↑(0 + 1) + 1) ^ 2

case nat.succ.succ.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑(0 + 1 + 1)) =
    preNormEDS b c d (↑(0 + 1 + 1) - 1) ^ 2 * preNormEDS b c d ↑(0 + 1 + 1) * preNormEDS b c d (↑(0 + 1 + 1) + 2) -
      preNormEDS b c d (↑(0 + 1 + 1) - 2) * preNormEDS b c d ↑(0 + 1 + 1) * preNormEDS b c d (↑(0 + 1 + 1) + 1) ^ 2

case nat.succ.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * ↑(m + 1 + 1 + 1)) =
    preNormEDS b c d (↑(m + 1 + 1 + 1) - 1) ^ 2 * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 2) -
      preNormEDS b c d (↑(m + 1 + 1 + 1) - 2) * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 1) ^ 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case nat.succ.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑(0 + 1)) =
    preNormEDS b c d (↑(0 + 1) - 1) ^ 2 * preNormEDS b c d ↑(0 + 1) * preNormEDS b c d (↑(0 + 1) + 2) -
      preNormEDS b c d (↑(0 + 1) - 2) * preNormEDS b c d ↑(0 + 1) * preNormEDS b c d (↑(0 + 1) + 1) ^ 2

pp: case nat.succ.succ.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑(0 + 1 + 1)) =
    preNormEDS b c d (↑(0 + 1 + 1) - 1) ^ 2 * preNormEDS b c d ↑(0 + 1 + 1) * preNormEDS b c d (↑(0 + 1 + 1) + 2) -
      preNormEDS b c d (↑(0 + 1 + 1) - 2) * preNormEDS b c d ↑(0 + 1 + 1) * preNormEDS b c d (↑(0 + 1 + 1) + 1) ^ 2

pp: case nat.succ.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * ↑(m + 1 + 1 + 1)) =
    preNormEDS b c d (↑(m + 1 + 1 + 1) - 1) ^ 2 * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 2) -
      preNormEDS b c d (↑(m + 1 + 1 + 1) - 2) * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 1) ^ 2

Tactic:
simp

Goal state after:
case nat.succ.succ.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑(0 + 1 + 1)) =
    preNormEDS b c d (↑(0 + 1 + 1) - 1) ^ 2 * preNormEDS b c d ↑(0 + 1 + 1) * preNormEDS b c d (↑(0 + 1 + 1) + 2) -
      preNormEDS b c d (↑(0 + 1 + 1) - 2) * preNormEDS b c d ↑(0 + 1 + 1) * preNormEDS b c d (↑(0 + 1 + 1) + 1) ^ 2

case nat.succ.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * ↑(m + 1 + 1 + 1)) =
    preNormEDS b c d (↑(m + 1 + 1 + 1) - 1) ^ 2 * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 2) -
      preNormEDS b c d (↑(m + 1 + 1 + 1) - 2) * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 1) ^ 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case nat.succ.succ.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑(0 + 1 + 1)) =
    preNormEDS b c d (↑(0 + 1 + 1) - 1) ^ 2 * preNormEDS b c d ↑(0 + 1 + 1) * preNormEDS b c d (↑(0 + 1 + 1) + 2) -
      preNormEDS b c d (↑(0 + 1 + 1) - 2) * preNormEDS b c d ↑(0 + 1 + 1) * preNormEDS b c d (↑(0 + 1 + 1) + 1) ^ 2

pp: case nat.succ.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * ↑(m + 1 + 1 + 1)) =
    preNormEDS b c d (↑(m + 1 + 1 + 1) - 1) ^ 2 * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 2) -
      preNormEDS b c d (↑(m + 1 + 1 + 1) - 2) * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 1) ^ 2

Tactic:
simp

Goal state after:
case nat.succ.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * ↑(m + 1 + 1 + 1)) =
    preNormEDS b c d (↑(m + 1 + 1 + 1) - 1) ^ 2 * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 2) -
      preNormEDS b c d (↑(m + 1 + 1 + 1) - 2) * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 1) ^ 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case nat.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑0 + 1) =
    (preNormEDS b c d (↑0 + 2) * preNormEDS b c d ↑0 ^ 3 * if Even ↑0 then b else 1) -
      preNormEDS b c d (↑0 - 1) * preNormEDS b c d (↑0 + 1) ^ 3 * if Even ↑0 then 1 else b

pp: case nat.succ.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑(0 + 1) + 1) =
    (preNormEDS b c d (↑(0 + 1) + 2) * preNormEDS b c d ↑(0 + 1) ^ 3 * if Even ↑(0 + 1) then b else 1) -
      preNormEDS b c d (↑(0 + 1) - 1) * preNormEDS b c d (↑(0 + 1) + 1) ^ 3 * if Even ↑(0 + 1) then 1 else b

pp: case nat.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
n✝ : ℕ
⊢ preNormEDS b c d (2 * ↑(n✝ + 1 + 1) + 1) =
    (preNormEDS b c d (↑(n✝ + 1 + 1) + 2) * preNormEDS b c d ↑(n✝ + 1 + 1) ^ 3 * if Even ↑(n✝ + 1 + 1) then b else 1) -
      preNormEDS b c d (↑(n✝ + 1 + 1) - 1) * preNormEDS b c d (↑(n✝ + 1 + 1) + 1) ^ 3 *
        if Even ↑(n✝ + 1 + 1) then 1 else b

Tactic:
simp

Goal state after:
case nat.succ.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑(0 + 1) + 1) =
    (preNormEDS b c d (↑(0 + 1) + 2) * preNormEDS b c d ↑(0 + 1) ^ 3 * if Even ↑(0 + 1) then b else 1) -
      preNormEDS b c d (↑(0 + 1) - 1) * preNormEDS b c d (↑(0 + 1) + 1) ^ 3 * if Even ↑(0 + 1) then 1 else b

case nat.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
n✝ : ℕ
⊢ preNormEDS b c d (2 * ↑(n✝ + 1 + 1) + 1) =
    (preNormEDS b c d (↑(n✝ + 1 + 1) + 2) * preNormEDS b c d ↑(n✝ + 1 + 1) ^ 3 * if Even ↑(n✝ + 1 + 1) then b else 1) -
      preNormEDS b c d (↑(n✝ + 1 + 1) - 1) * preNormEDS b c d (↑(n✝ + 1 + 1) + 1) ^ 3 *
        if Even ↑(n✝ + 1 + 1) then 1 else b
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case nat.succ.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑(0 + 1) + 1) =
    (preNormEDS b c d (↑(0 + 1) + 2) * preNormEDS b c d ↑(0 + 1) ^ 3 * if Even ↑(0 + 1) then b else 1) -
      preNormEDS b c d (↑(0 + 1) - 1) * preNormEDS b c d (↑(0 + 1) + 1) ^ 3 * if Even ↑(0 + 1) then 1 else b

pp: case nat.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
n✝ : ℕ
⊢ preNormEDS b c d (2 * ↑(n✝ + 1 + 1) + 1) =
    (preNormEDS b c d (↑(n✝ + 1 + 1) + 2) * preNormEDS b c d ↑(n✝ + 1 + 1) ^ 3 * if Even ↑(n✝ + 1 + 1) then b else 1) -
      preNormEDS b c d (↑(n✝ + 1 + 1) - 1) * preNormEDS b c d (↑(n✝ + 1 + 1) + 1) ^ 3 *
        if Even ↑(n✝ + 1 + 1) then 1 else b

Tactic:
simp

Goal state after:
case nat.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
n✝ : ℕ
⊢ preNormEDS b c d (2 * ↑(n✝ + 1 + 1) + 1) =
    (preNormEDS b c d (↑(n✝ + 1 + 1) + 2) * preNormEDS b c d ↑(n✝ + 1 + 1) ^ 3 * if Even ↑(n✝ + 1 + 1) then b else 1) -
      preNormEDS b c d (↑(n✝ + 1 + 1) - 1) * preNormEDS b c d (↑(n✝ + 1 + 1) + 1) ^ 3 *
        if Even ↑(n✝ + 1 + 1) then 1 else b
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
⊢ preNormEDS b c d (2 * -↑0 + 1) =
    (preNormEDS b c d (-↑0 + 2) * preNormEDS b c d (-↑0) ^ 3 * if Even (-↑0) then b else 1) -
      preNormEDS b c d (-↑0 - 1) * preNormEDS b c d (-↑0 + 1) ^ 3 * if Even (-↑0) then 1 else b

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case nat.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ complEDS b c d k (2 * ↑0) = complEDS b c d k ↑0 * complEDS₂ b c d (↑0 * k)

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case nat.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ complEDS b c d k (2 * ↑0 + 1) =
    complEDS b c d k ↑0 ^ 2 * normEDS b c d ((↑0 + 1) * k + 1) * normEDS b c d ((↑0 + 1) * k - 1) -
      complEDS b c d k (↑0 + 1) ^ 2 * normEDS b c d (↑0 * k + 1) * normEDS b c d (↑0 * k - 1)

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (2 * ↑n + 1) =
      complEDS b c d k ↑n ^ 2 * normEDS b c d ((↑n + 1) * k + 1) * normEDS b c d ((↑n + 1) * k - 1) -
        complEDS b c d k (↑n + 1) ^ 2 * normEDS b c d (↑n * k + 1) * normEDS b c d (↑n * k - 1)
⊢ complEDS b c d k (2 * -↑0 + 1) =
    complEDS b c d k (-↑0) ^ 2 * normEDS b c d ((-↑0 + 1) * k + 1) * normEDS b c d ((-↑0 + 1) * k - 1) -
      complEDS b c d k (-↑0 + 1) ^ 2 * normEDS b c d (-↑0 * k + 1) * normEDS b c d (-↑0 * k - 1)

Tactic:
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)
J : Type u_1
inst✝ : Finite J
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
j : J → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
val✝ : Fintype J
i : I
fi : ∀ {X : I}, X ∈ Finset.image j Finset.univ → Nonempty (i ⟶ X)
k : J
⊢ j k ∈ Finset.image j Finset.univ

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
⊢ f (preNormEDS' b c d 0) = preNormEDS' (f b) (f c) (f d) 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case one
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
⊢ f (preNormEDS' b c d 1) = preNormEDS' (f b) (f c) (f d) 1

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case two
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
⊢ f (preNormEDS' b c d 2) = preNormEDS' (f b) (f c) (f d) 2

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case three
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
⊢ f (preNormEDS' b c d 3) = preNormEDS' (f b) (f c) (f d) 3

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case four
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
⊢ f (preNormEDS' b c d 4) = preNormEDS' (f b) (f c) (f d) 4

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case intro.refine_1
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)
J : Type u_1
inst✝ : Finite J
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
j : J → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
val✝ : Fintype J
i : I
fi : (k : J) → i ⟶ j k
k : I
fkj : k ⟶ i
e : D.map fkj ⁻¹ᵁ ⨆ k, D.map (fi k) ⁻¹ᵁ V k = ⊤
⊢ ⨆ i_1, D.map (fkj ≫ fi i_1) ⁻¹ᵁ V i_1 ≤ ⨆ x, D.map (fkj ≫ fi x) ⁻¹ᵁ V x

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
k : ℤ
⊢ f (complEDS' b c d k 0) = complEDS' (f b) (f c) (f d) k 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case one
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
k : ℤ
⊢ f (complEDS' b c d k 1) = complEDS' (f b) (f c) (f d) k 1

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_3.refine_4
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)), IsOpenImmersion.lift (𝒰.f k) s.snd ⋯ ≫ 𝒰.f k = s.snd

Tactic:
simp

Goal state after:
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
⊢ (fun xy ↦ ∃ (h : W'.Nonsingular xy.1 xy.2), Point.some xy.1 xy.2 h ∈ Set.univ) = fun xy ↦ W'.Nonsingular xy.1 xy.2

Tactic:
simp

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✝² : IsAffine S
inst✝¹ : IsAffine X
inst✝ : ∀ (i : I), IsAffine (D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
⊢ ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i

Tactic:
wlog hS : ∃ R, S = Spec R generalizing S

Goal state after:
case inr
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✝² : IsAffine S
inst✝¹ : IsAffine X
inst✝ : ∀ (i : I), IsAffine (D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
this :
  ∀ {S : Scheme} (t : D ⟶ (Functor.const I).obj S) (f : X ⟶ S) [LocallyOfFinitePresentation f] [IsAffine S],
    c.π ≫ t = (Functor.const I).map (a ≫ f) → (∃ R, S = Spec R) → ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i
hS : ¬∃ R, S = Spec R
⊢ ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i

I : Type u
inst✝⁵ : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : IsAffine X
inst✝² : ∀ (i : I), IsAffine (D.obj i)
a : c.pt ⟶ X
S : Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : IsAffine S
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
hS : ∃ R, S = Spec R
⊢ ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i
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'
⊢ (fun xy ↦ ∃ (h : W'.Equation xy.1 xy.2), Point.mk h ∈ Set.univ) = fun xy ↦ W'.Equation xy.1 xy.2

Tactic:
simp

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

Goal state before:
pp: 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
p : W.CoordinateRing
h0 : p ≠ 0
hp : CoordinateRing.XYIdeal W x✝ (C y✝) = span {p}
⊢ finrank F (W.CoordinateRing ⧸ span {p}) = 1

Tactic:
← (quotientEquivAlgOfEq F hp).toLinearEquiv.finrank_eq,

Goal state after:
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
p : W.CoordinateRing
h0 : p ≠ 0
hp : CoordinateRing.XYIdeal W x✝ (C y✝) = span {p}
⊢ finrank F (W.CoordinateRing ⧸ CoordinateRing.XYIdeal W x✝ (C y✝)) = 1