mathlib-initiative/mathlib-tactics huggingface dataset:
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 : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x | ∃ i V, ∃ (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact ↑(sSup s)
this : Finite ↑s
i : ↑s → I
V : (x : ↑s) → (D.obj (i x)).Opens
hV : ∀ (x : ↑s), IsAffineOpen (V x)
hVi : ∀ (x : ↑s), c.π.app (i x) ⁻¹ᵁ V x = ↑x
x : ↥hsf.toFinset
⊢ ↑x ∈ s

Tactic:
by simpa only [Set.Finite.mem_toFinset] using x.2

Goal state after:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
V : Opens (X i)
hV : IsCompact ↑V
⊢ ∀ (i_1 : ι) (h : i_1 ∈ {i}), IsCompact ((fun j hj ↦ ⋯ ▸ V) i_1 h).carrier

Tactic:
by rintro i rfl; simpa

Goal state after:
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : Surjective f
inst✝ : QuasiCompact f
⊢ EffectiveEpi f.base

Tactic:
rw [TopCat.effectiveEpi_iff_isQuotientMap]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : Surjective f
inst✝ : QuasiCompact f
⊢ Topology.IsQuotientMap ⇑f
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
y : R[X]
⊢ (Y - C y).natDegree < W'.polynomial.natDegree

Tactic:
rw [natDegree_polynomial, natDegree_X_sub_C]; norm_num1

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

Goal state before:
pp: 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))
H : Ideal.span s₀ ≤ RingHom.ker g
q₁ : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)
q₂ : MvPolynomial (Fin m) R
hq₁ : q₁ ∈ Ideal.span s₀
q₃ : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)
q₄ : MvPolynomial (Fin m) R
hq₃ : q₃ ∈ Ideal.span s₀
⊢ (commAlgEquiv R (Fin n) (Fin m)).symm (q₁ + σ q₂) + (commAlgEquiv R (Fin n) (Fin m)).symm (q₃ + σ q₄) =
    (commAlgEquiv R (Fin n) (Fin m)).symm (q₁ + q₃ + σ (q₂ + q₄))

Tactic:
by simp only [map_add, add_add_add_comm]

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 c * atom W b d + atom W a d * atom W b c =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c

Tactic:
atom_neg_right

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 (-c) * atom W b d + atom W a d * atom W b (-c) =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c

Tactic:
atom_neg_right

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
⊢ atom W a b * atom W c (-d) - atom W a c * atom W b (-d) + atom W a (-d) * atom W b c =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c

Tactic:
atom_neg_right

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

Goal state before:
pp: case neg.some.none
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + q.degree + 1
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
hq' : q.degree = none
⊢ (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 • some dp) (2 • none + 3)

pp: case neg.some.some
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + q.degree + 1
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hq' : q.degree = some dq
⊢ (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 • some dp) (2 • some dq + 3)

Tactic:
· exact (hq hq').elim

Goal state after:
case neg.some.some
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + q.degree + 1
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hq' : q.degree = some dq
⊢ (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 • some dp) (2 • some dq + 3)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.ψ₂ ^ 2 = C W.Ψ₂Sq + 4 * W.toAffine.polynomial

Tactic:
simp [C_Ψ₂Sq]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (mk W) W.ψ₂ ^ 2 = (mk W) (C W.Ψ₂Sq)

Tactic:
simp [C_Ψ₂Sq]

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ max (2 • p.degree) (2 • q.degree + 3) ≠ 1

Tactic:
rcases p.degree with (_ | _ | _ | _)

Goal state after:
case none
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ max (2 • none) (2 • q.degree + 3) ≠ 1

case some.zero
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ max (2 • some 0) (2 • q.degree + 3) ≠ 1

case some.succ.zero
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ max (2 • some (0 + 1)) (2 • q.degree + 3) ≠ 1

case some.succ.succ
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
n✝ : ℕ
⊢ max (2 • some (n✝ + 1 + 1)) (2 • q.degree + 3) ≠ 1
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 : I), IsAffine (D.obj i)
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝⁴ : IsAffine (Spec R)
S : CommRingCat
inst✝³ : IsAffine (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst✝² : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine (D.obj i)]
    (t : D ⟶ (Functor.const I).obj (Spec R)) (a : c.pt ⟶ Spec S),
    c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ) →
      (∃ D', D = D' ⋙ Scheme.Spec) → ∃ i g, c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst✝¹ : ∀ (i : I), IsIso (e.app i)
inst✝ : IsIso e
inst : ∀ (i : I), IsAffine ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
i : I
g : (D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i ⟶ Spec S
hg : ((Cone.postcompose (asIso e).hom).obj c).π.app i ≫ g = a
hg' : g ≫ Spec.map φ = (inv e ≫ t).app i
⊢ (e.app i ≫ g) ≫ Spec.map φ = t.app i

Tactic:
by simp [hg']

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
inst✝¹² : DecidableEq F
inst✝¹¹ : DecidableEq K
inst✝¹⁰ : DecidableEq L
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x₁ y₁ : F
h₁ : (W'⁄F).Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂
⊢ f y₁ = (W'⁄K).negY (f x₂) (f y₂)

Tactic:
hxy.right,

Goal state after:
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✝¹² : DecidableEq F
inst✝¹¹ : DecidableEq K
inst✝¹⁰ : DecidableEq L
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x₁ y₁ : F
h₁ : (W'⁄F).Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂
⊢ f ((W'⁄F).negY x₂ y₂) = (W'⁄K).negY (f x₂) (f y₂)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case h.a₃
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero 2
u : F
hu : u ^ 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
⊢ ({ u := Units.mk0 u hu0, r := 0, s := 0, t := 0 } • E).a₃ = E'.a₃

pp: case h.a₄
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero 2
u : F
hu : u ^ 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
⊢ ({ u := Units.mk0 u hu0, r := 0, s := 0, t := 0 } • E).a₄ = E'.a₄

pp: case h.a₆
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero 2
u : F
hu : u ^ 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
⊢ ({ u := Units.mk0 u hu0, r := 0, s := 0, t := 0 } • E).a₆ = E'.a₆

Tactic:
· simp_rw [variableChange_a₃, a₁_of_isCharThreeJNeZeroNF, a₃_of_isCharThreeJNeZeroNF]
    ring1

Goal state after:
case h.a₄
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero 2
u : F
hu : u ^ 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
⊢ ({ u := Units.mk0 u hu0, r := 0, s := 0, t := 0 } • E).a₄ = E'.a₄

case h.a₆
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero 2
u : F
hu : u ^ 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
⊢ ({ u := Units.mk0 u hu0, r := 0, s := 0, t := 0 } • E).a₆ = E'.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case h.a₆
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 := ⋯
this : Invertible 3 := ⋯
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'.a₆ ≠ 0
u : F
hu : u ^ 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ ({ u := Units.mk0 u hu0, r := 0, s := 0, t := 0 } • E).a₆ = E'.a₆

Tactic:
simp_rw [variableChange_a₆, a₁_of_isShortNF, a₂_of_isShortNF, a₃_of_isShortNF,
        ha₄, Units.val_inv_eq_inv_val, Units.val_mk0, inv_pow, inv_mul_eq_div, hu]

Goal state after:
case h.a₆
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'.a₆ ≠ 0
u : F
hu : u ^ 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ (E.a₆ + 0 * 0 + 0 ^ 2 * 0 + 0 ^ 3 - 0 * 0 - 0 ^ 2 - 0 * 0 * 0) / (E.a₆ / E'.a₆) = E'.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < n
h : ↑n ≠ 0
⊢ 0 < (W.preΨ' n).natDegree

Tactic:
W.natDegree_preΨ' h,

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < n
h : ↑n ≠ 0
⊢ 0 < (n ^ 2 - if Even n then 4 else 1) / 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑n ≠ 0
⊢ (W.preΨ' n).coeff (W.preΨ' n).natDegree = ↑(if Even n then n / 2 else n)

Tactic:
W.natDegree_preΨ' h,

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑n ≠ 0
⊢ (W.preΨ' n).coeff ((n ^ 2 - if Even n then 4 else 1) / 2) = ↑(if Even n then n / 2 else n)
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 (W.ΨSq n).natDegree = ↑n ^ 2

Tactic:
W.natDegree_ΨSq h,

Goal state after:
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
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑↑(m + 1) ≠ 0
hn : m = 0
hm : (↑(m + 1)).natAbs = m + 1
h' : 1 = 0
⊢ C ↑↑(m + 1) = C 0

Tactic:
by push_cast [hn, C_neg, C_1, h', neg_zero, C_0]; rfl

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
m : ℕ
h : ↑(-↑(m + 1)) ≠ 0
hn : m = 0
hm : (-↑(m + 1)).natAbs = m + 1
h' : 1 = 0
⊢ C ↑(-↑(m + 1)) = C 0

Tactic:
by push_cast [hn, C_neg, C_1, h', neg_zero, C_0]; rfl

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
heq : E.j = E'.j
p : ℕ
h✝ : CharP F p
hchar2 : p = 2
⊢ ∃ C, C • E = E'

pp: case neg
F : Type u_1
inst✝³ : Field F
inst✝² : IsSepClosed F
E E' : WeierstrassCurve F
inst✝¹ : E.IsElliptic
inst✝ : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h✝ : CharP F p
hchar2 : ¬p = 2
⊢ ∃ C, C • E = E'

Tactic:
· subst hchar2
    exact exists_variableChange_of_char_two _ _ heq

Goal state after:
case neg
F : Type u_1
inst✝³ : Field F
inst✝² : IsSepClosed F
E E' : WeierstrassCurve F
inst✝¹ : E.IsElliptic
inst✝ : E'.IsElliptic
heq : E.j = E'.j
p : ℕ
h✝ : CharP F p
hchar2 : ¬p = 2
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case neg
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Jacobian R
W : Jacobian F
inst✝ : DecidableEq F
point✝ : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P)
hPz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (fromAffine (toAffine W P)).point =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }.point

Tactic:
toAffine_of_Z_ne_zero hP hPz

Goal state after:
case neg
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Jacobian R
W : Jacobian F
inst✝ : DecidableEq F
point✝ : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P)
hPz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: R K : Type u
inst✝² : Ring R
inst✝¹ : DivisionRing K
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (s : Set R), s ∈ 𝓝 0 ↔ ∃ γ, {x | v.restrict x < ↑γ} ⊆ s

Tactic:
by
      let := @IsTopologicalAddGroup.rightUniformSpace R _ v.subgroups_basis.topology _
      intro s
      rw [Filter.hasBasis_iff.mp v.subgroups_basis.hasBasis_nhds_zero s]
      simp_rw [restrict_lt_iff_lt_embedding]
      exact exists_congr fun γ ↦ by rw [true_and]; rfl

Goal state after:
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 x : R
y : ↥(posSubmonoid R)
h : ValueGroupWithZero.mk x y ≠ 0
⊢ ValueGroupWithZero.mk x y * (ValueGroupWithZero.mk x y)⁻¹ = 1

Tactic:
by
    rw [ne_eq, ← ValueGroupWithZero.mk_zero 1, ValueGroupWithZero.mk_eq_mk] at h
    simp only [Submonoid.coe_one, mul_one, zero_mul, zero_vle, and_true] at h
    grw [ValueGroupWithZero.inv_mk x y h, ← ValueGroupWithZero.mk_one_one,
      ValueGroupWithZero.mk_mul_mk, ValueGroupWithZero.mk_eq_mk, veq_mul_comm x]
    simp

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

Goal state before:
pp: K : Type u_2
inst✝¹ : DivisionRing K
inst✝ : ValuativeRel K
a : K
⊢ a ≤ᵥ 0 ↔ a = 0

Tactic:
← supp_def,

Goal state after:
K : Type u_2
inst✝¹ : DivisionRing K
inst✝ : ValuativeRel K
a : K
⊢ a ∈ supp K ↔ a = 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr✝ : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
hγ : v r ≠ 0
hγ' : v r ≤ v ↑s → v r < v ↑s
hr : ¬v r = 1
⊢ v r ≠ 0

Tactic:
by simpa using hγ

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

Goal state before:
pp: case refine_2
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : IsUniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
hfg : Continuous (⇑f + ⇑g)
x : Completion α
⊢ ∀ (a : α), ((f + g).completion ⋯) ↑a = (f.completion hf + g.completion hg) ↑a

Tactic:
simp [(f + g).completion_coe hfg, coe_add, f.completion_coe hf, g.completion_coe hg]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
⊢ Cauchy (map (fun x ↦ ↑x⁻¹) (Filter.comap coe' (𝓝 y)))

Tactic:
have : (fun (x : K) => (↑x⁻¹ : hat K)) =
      ((fun (y : K) => (↑y : hat K)) ∘ (fun (x : K) => (x⁻¹ : K))) := by
    simp [Function.comp_def]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
⊢ Cauchy (map (fun x ↦ ↑x⁻¹) (Filter.comap coe' (𝓝 y)))
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : ValuativeRel A
inst✝² : ValuativeRel B
inst✝¹ : Algebra A B
inst✝ : ValuativeExtension A B
x✝ : ↥(posSubmonoid A)
a : A
ha : a ∈ posSubmonoid A
⊢ (algebraMap A B) a ∈ posSubmonoid B

Tactic:
by simpa only [posSubmonoid_def, ← (algebraMap A B).map_zero, vlt_iff_vlt] using ha

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

Goal state before:
pp: R✝ : Type u_1
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
x : (ofClass Valued.v).ValueGroup₀
⊢ (WithZero.map' ↑(valueGroupEquiv v).symm) ((WithZero.map' ↑(valueGroupEquiv v)) x) = x

Tactic:
match x with
    | 0 => simp
    | .coe a => simp

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

Goal state before:
pp: case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
h_res : v.restrict.IsEquiv w.restrict
x : (ofClass Valued.v).ValueGroup₀ˣ
u : ↥(ofClass Valued.v).valueGroup := WithZero.unzero ⋯
a : R
ha : (ofClass Valued.v) a ≠ 0
y✝ : R
hu : (ofClass Valued.v) a * ↑↑u = (ofClass Valued.v) y✝
y₀ : (ofClass Valued.v).ValueGroup₀ := h_val.orderMonoidIso ↑x
hy₀_def : y₀ = h_val.orderMonoidIso ↑x
hy₀_ne_zero : y₀ ≠ 0
y : (ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 y₀ hy₀_ne_zero
hy_def : y = Units.mk0 y₀ hy₀_ne_zero
b : R
hb : Valued.v.restrict b < ↑y
⊢ Valued.v.restrict b < ↑x

Tactic:
← h_val.orderMonoidIso_spec,

Goal state after:
case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
h_res : v.restrict.IsEquiv w.restrict
x : (ofClass Valued.v).ValueGroup₀ˣ
u : ↥(ofClass Valued.v).valueGroup := WithZero.unzero ⋯
a : R
ha : (ofClass Valued.v) a ≠ 0
y✝ : R
hu : (ofClass Valued.v) a * ↑↑u = (ofClass Valued.v) y✝
y₀ : (ofClass Valued.v).ValueGroup₀ := h_val.orderMonoidIso ↑x
hy₀_def : y₀ = h_val.orderMonoidIso ↑x
hy₀_ne_zero : y₀ ≠ 0
y : (ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 y₀ hy₀_ne_zero
hy_def : y = Units.mk0 y₀ hy₀_ne_zero
b : R
hb : h_val.orderMonoidIso (Valued.v.restrict b) < ↑y
⊢ Valued.v.restrict b < ↑x