mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RingHom.PurelyInseparable

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Field K
f : F →+* E
g : E →+* K
hf : f.IsPurelyInseparable
hg : g.IsPurelyInseparable
algInst✝² : Algebra F E := f.toAlgebra
algInst✝¹ : Algebra E K := g.toAlgebra
algInst✝ : Algebra F K := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower F E K := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap F K))
algebraizeInst✝¹ : IsPurelyInseparable F E
algebraizeInst✝ : IsPurelyInseparable E K
⊢ (g.comp f).IsPurelyInseparable

Tactic:
exact IsPurelyInseparable.trans F E K

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
⊢ TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (X.directedAffineCover.f i))

Tactic:
convert! X.isBasis_affineOpens

Goal state after:
P : MorphismProperty Scheme
X : Scheme
⊢ (Set.range fun i ↦ Hom.opensRange (X.directedAffineCover.f i)) = X.affineOpens
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{?u.7, ?u.34} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, ?u.34} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : d.cover.I₀
x : ↥(pullback (d.cover.f i) (d.cover.f j))
⊢ ∃ k hki hkj y, (pullback.lift (d.functor.map hki) (d.functor.map hkj) ⋯) y = x

Tactic:
let xi := pullback.fst (d.cover.f i) _ x

Goal state after:
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{?u.7, ?u.61} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, ?u.61} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : d.cover.I₀
x : ↥(pullback (d.cover.f i) (d.cover.f j))
xi : ↥(d.cover.X i) := (pullback.fst (d.cover.f i) (d.cover.f j)) x
⊢ ∃ k hki hkj y, (pullback.lift (d.functor.map hki) (d.functor.map hkj) ⋯) y = x
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{?u.7, ?u.114} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, ?u.114} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : d.cover.I₀
x : ↥(pullback (d.cover.f i) (d.cover.f j))
xi : ↥(d.cover.X i) := (pullback.fst (d.cover.f i) (d.cover.f j)) x
xj : ↥(d.cover.X j) := (pullback.snd (d.cover.f i) (d.cover.f j)) x
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1 : (trans 𝒰 fi) uk = (d.natTrans.app i) xi
h2 : (trans 𝒰 fj) uk = (d.natTrans.app j) xj
⊢ (d.natTrans.app j ≫ 𝒰.f j) xj = (𝒰.f j) ((trans 𝒰 fj) uk)

Tactic:
simp [xj, h2]

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

Goal state before:
pp: R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
this : coeff(f) = ⋃ i, ⋃ (_ : i < f.natDegree + 2), {f.coeff i}
⊢ ConstructibleSetData.toSet
      (Finset.image (fun j ↦ { f := f.coeff j, n := 0, g := 0 }) (Finset.range (f.natDegree + 2))) =
    (zeroLocus coeff(f))ᶜ

Tactic:
by
          simp [BasicConstructibleSetData.toSet, ConstructibleSetData.toSet,
            ← Set.compl_eq_univ_sdiff, eq_compl_comm (y := zeroLocus _), ← zeroLocus_iUnion₂, this]

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)
U : Set S
κ : Type u_4
inst✝ : Finite κ
s : κ → Set S
hs : ⋃ i, s i = U
H : ∀ (i : κ), IsCompactOpenCovered f (s i)
V : κ → Opens ((i : ι) × X i)
hVeq : ∀ (i : κ), IsCompact (V i).carrier
hVc : ∀ (i : κ), (fun x ↦ f x.fst x.snd) '' (V i).carrier = s i
⊢ (fun p ↦ f p.fst p.snd) '' (⨆ i, V i).carrier = U

Tactic:
simp_all [Set.image_iUnion, ← hs]

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
e : C ≌ D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
this : True → e.functor.map g₁ ≫ ε a₁ = e.functor.map g₂ ≫ ε a₂
⊢ True

Tactic:
trivial

Goal state after:
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
b : ↑Y.toPresheafedSpace ⟶ ↑S.toPresheafedSpace
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun V ↦ (↑V).1) ⋯
i : 𝒰.I₀
this : IsAffine (𝒰.X i)
⊢ Set.range ⇑(TopCat.Hom.hom (𝒰.f i).base) ⊆ ↑(↑i).1

Tactic:
by simp [𝒰]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
b : ↑Y.toPresheafedSpace ⟶ ↑S.toPresheafedSpace
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun V ↦ (↑V).1) ⋯
i : 𝒰.I₀
this : IsAffine (𝒰.X i)
f' : pullback π (𝒰.f i) ⟶ ↑↑(↑i).2 := IsOpenImmersion.lift (Opens.ι ↑(↑i).2) (fst π (𝒰.f i) ≫ f) ⋯
h1 :
  fst (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i) =
    map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯ ≫ fst π π
h2 :
  snd (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i) =
    map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯ ≫ snd π π
u : 𝒰.X i ⟶ ↑↑(↑i).2
hu : snd π (𝒰.f i) ≫ u = f'
⊢ ∃ u, fst π (𝒰.f i) ≫ f = snd π (𝒰.f i) ≫ u

Tactic:
refine ⟨u ≫ Scheme.Opens.ι _, ?_⟩

Goal state after:
X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
b : ↑Y.toPresheafedSpace ⟶ ↑S.toPresheafedSpace
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun V ↦ (↑V).1) ⋯
i : 𝒰.I₀
this : IsAffine (𝒰.X i)
f' : pullback π (𝒰.f i) ⟶ ↑↑(↑i).2 := IsOpenImmersion.lift (Opens.ι ↑(↑i).2) (fst π (𝒰.f i) ≫ f) ⋯
h1 :
  fst (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i) =
    map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯ ≫ fst π π
h2 :
  snd (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i) =
    map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯ ≫ snd π π
u : 𝒰.X i ⟶ ↑↑(↑i).2
hu : snd π (𝒰.f i) ≫ u = f'
⊢ fst π (𝒰.f i) ≫ f = snd π (𝒰.f i) ≫ u ≫ Opens.ι ↑(↑i).2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ (W.map f).Δ = f ↑W.Δ'

Tactic:
map_Δ,

Goal state after:
R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ f W.Δ = f ↑W.Δ'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
⊢ 1 < (f + g).degree

Tactic:
rcases Nat.WithBot.add_eq_three_iff.mp h0.symm with h | h | h | h

Goal state after:
case inl
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 0 ∧ g.degree = 3
⊢ 1 < (f + g).degree

case inr.inl
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 1 ∧ g.degree = 2
⊢ 1 < (f + g).degree

case inr.inr.inl
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 2 ∧ g.degree = 1
⊢ 1 < (f + g).degree

case inr.inr.inr
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
⊢ 1 < (f + g).degree
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case e'_2
I : Type u
inst✝³ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
U : ↥(D.obj i) → (D.obj i).Opens
hU : ∀ (x : ↥(D.obj i)), IsAffineOpen (U x)
hxU : ∀ (x : ↥(D.obj i)), x ∈ U x
j : ↥(D.obj i) → I
f : (x : ↥(D.obj i)) → j x ⟶ i
H : ∀ (x : ↥(D.obj i)), (ConcreteCategory.hom (Scheme.Hom.app (D.map (f x)) (U x))) ((s |_ U x) ⋯) = 0
t : Finset ↥(D.obj i)
ht : ⋃ x ∈ t, ↑(U x) = ⊤
k : I
fk : {X : I} → X ∈ insert i (Finset.image j t) → (k ⟶ X)
hk :
  ∀ {X Y : I} (mX : X ∈ insert i (Finset.image j t)) (mY : Y ∈ insert i (Finset.image j t)) {f_1 : X ⟶ Y},
    ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ Finset.image (fun x ↦ ⟨j ↑x, ⟨i, ⟨⋯, ⟨⋯, f ↑x⟩⟩⟩⟩) t.attach → fk mX ≫ f_1 = fk mY
x : ↥(D.obj k)
l : ↥(D.obj i)
hl : l ∈ t
hlU : (D.map (fk ⋯)) x ∈ ↑(U l)
h₁ : fk ⋯ = fk ⋯ ≫ f l
h₂ : D.map (fk ⋯) ⁻¹ᵁ U l ≤ D.map (fk ⋯) ⁻¹ᵁ D.map (f l) ⁻¹ᵁ U l
⊢ (ConcreteCategory.hom ((D.obj k).presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (Scheme.Hom.appTop (D.map (fk ⋯)))) s) =
    (ConcreteCategory.hom (Scheme.Hom.appLE (D.map (fk ⋯)) (D.map (f l) ⁻¹ᵁ U l) (D.map (fk ⋯) ⁻¹ᵁ U l) h₂))
      ((ConcreteCategory.hom (Scheme.Hom.app (D.map (f l)) (U l)))
        ((ConcreteCategory.hom ((D.obj i).presheaf.map (homOfLE ⋯).op)) s))

Tactic:
simp [Scheme.Hom.app_eq_appLE, ← ConcreteCategory.comp_apply, -CommRingCat.hom_comp,
      Scheme.Hom.appLE_comp_appLE, ← Functor.map_comp, h₁]

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

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

Tactic:
have Y_sq : mk W' Y ^ 2 = mk W' (C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) -
      C (C W'.a₁ * X + C W'.a₃) * Y) := AdjoinRoot.mk_eq_mk.mpr ⟨1, by rw [polynomial]; ring1⟩

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
Y_sq : (mk W') Y ^ 2 = (mk W') (C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) - C (C W'.a₁ * X + C W'.a₃) * Y)
⊢ (p • 1 + q • (mk W') Y) * (mk W') Y =
    (q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) • 1 + (p - q * (C W'.a₁ * X + C W'.a₃)) • (mk W') Y
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: 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
P : ℕ → Sort u_4
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x✝ : ℕ
ih : (k : ℕ) → k < 2 * (x✝ + 2) + 1 → P k
⊢ P (2 * (x✝ + 2) + 1)

Tactic:
apply odd <;> exact ih _ <| by linarith only

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case intro.refine_2
I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
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 = ⊤
k : J
⊢ c.π.app (j k) ⁻¹ᵁ V k = (c.π.app k✝ ≫ D.map (fkj ≫ fi k)) ⁻¹ᵁ V k

Tactic:
c.w

Goal state after:
case intro.refine_2
I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
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 = ⊤
k : J
⊢ c.π.app (j k) ⁻¹ᵁ V k = c.π.app (j k) ⁻¹ᵁ V k
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 F = 1

Tactic:
Module.finrank_self

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}
⊢ 1 = 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ W.c₆ = -216 * W.b₆

Tactic:
rw [c₆, b₂_of_isCharTwoJEqZeroNF, b₄_of_isCharTwoJEqZeroNF]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ -0 ^ 3 + 36 * 0 * (2 * W.a₄) - 216 * W.b₆ = -216 * W.b₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ W'.polynomialZ =
    C W'.a₁ * X * Y + C (3 * W'.a₃) * Y * Z ^ 2 -
      (C (2 * W'.a₂) * X ^ 2 * Z + C (4 * W'.a₄) * X * Z ^ 3 + C (6 * W'.a₆) * Z ^ 5)

Tactic:
rw [polynomialZ, polynomial]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ (pderiv z)
      (Y ^ 2 + C W'.a₁ * X * Y * Z + C W'.a₃ * Y * Z ^ 3 -
        (X ^ 3 + C W'.a₂ * X ^ 2 * Z ^ 2 + C W'.a₄ * X * Z ^ 4 + C W'.a₆ * Z ^ 6)) =
    C W'.a₁ * X * Y + C (3 * W'.a₃) * Y * Z ^ 2 -
      (C (2 * W'.a₂) * X ^ 2 * Z + C (4 * W'.a₄) * X * Z ^ 3 + C (6 * W'.a₆) * Z ^ 5)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case neg
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : ¬P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

Tactic:
exact ⟨(hu.unit * hv.unit) ^ 2, by convert! (add_smul_of_not_equiv h hu hv).symm⟩

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

Goal state before:
pp: case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (0, y)) (𝓝 ((0, y).1 * (0, y).2))

Tactic:
rw [zero_mul, nhds_prod_eq, nhds_of_ne_zero hy, prod_pure, tendsto_map'_iff]

Goal state after:
case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
⊢ Tendsto ((fun p ↦ p.1 * p.2) ∘ fun a ↦ (a, y)) (𝓝 0) (𝓝 0)
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : (ofClass v).ValueGroup₀
x : R
hx : r < v.restrict x
hx' : v.restrict x ≠ 0
⊢ ∃ γ, {y | v.restrict (y - x) < ↑γ} ⊆ {x | v.restrict x ≤ r}ᶜ

Tactic:
exact ⟨Units.mk0 _ hx', fun y hy hy' ↦ ne_of_lt hy <| map_sub_swap v.restrict x y ▸
      (Valuation.map_sub_eq_of_lt_left _ <| lt_of_le_of_lt hy' hx)⟩

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

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
γ : (ValueGroupWithZero R)ˣ
⊢ ∃ a b, (valuation R) ↑a / (valuation R) ↑b = ↑γ

Tactic:
by
  obtain ⟨a, b, hab⟩ := exists_valuation_div_valuation_eq γ.val
  lift a to posSubmonoid R using by
    contrapose! hab
    rw [posSubmonoid_def, not_vlt, ← valuation_eq_zero_iff] at hab
    simp [hab, eq_comm]
  use a, b

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
r : (ofClass v).ValueGroup₀
x : R
hx : r < v.restrict x
hx' : v.restrict x ≠ 0
⊢ ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ {x | v.restrict x ≤ r}ᶜ

Tactic:
exact ⟨Units.mk0 _ hx', fun y hy hy' ↦ ne_of_lt hy <| map_sub_swap v.restrict x y ▸
      (Valuation.map_sub_eq_of_lt_left _ <| lt_of_le_of_lt hy' hx)⟩

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

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
γ : (ofClass Valued.v).ValueGroup₀ˣ
⊢ ∃ ia, ∀ x ∈ {x | Valued.v.restrict x < ↑ia}, (equiv v) x ∈ {x | Valued.v.restrict x < ↑γ}

Tactic:
obtain ⟨r, s, hr₀, hs₀, hr⟩ := exists_div_eq_of_unit Valued.v γ

Goal state after:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : R
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
⊢ ∃ ia, ∀ x ∈ {x | Valued.v.restrict x < ↑ia}, (equiv v) x ∈ {x | Valued.v.restrict x < ↑γ}
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
⊢ ∃ ia, ∀ x ∈ {x | Valued.v.restrict x < ↑ia}, (equiv v).symm x ∈ {x | Valued.v.restrict x < ↑γ}

Tactic:
obtain ⟨r, s, hr₀, hs₀, hr⟩ := exists_div_eq_of_unit Valued.v γ

Goal state after:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
⊢ ∃ ia, ∀ x ∈ {x | Valued.v.restrict x < ↑ia}, (equiv v).symm x ∈ {x | Valued.v.restrict x < ↑γ}
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation π ^ m ≤ 1
h_mn : m ≤ n
⊢ ∃ a, (algebraMap A K) a = x

Tactic:
use u * π ^ (n - m) * w.2

Goal state after:
case h
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation π ^ m ≤ 1
h_mn : m ≤ n
⊢ (algebraMap A K) (↑u * π ^ (n - m) * w.inv) = x
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H✝ : DenselyOrdered ↑s
this : (some ⁻¹' s).Subsingleton
x y : ↑s
H : x < y
z : ↑s
hz : x < z
hz' : z < y
hz0 : ⊥ < ↑z
⊢ ↑((↑z).unbot ⋯) < ↑((↑y).unbot ⋯)

Tactic:
WithBot.coe_unbot,

Goal state after:
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H✝ : DenselyOrdered ↑s
this : (some ⁻¹' s).Subsingleton
x y : ↑s
H : x < y
z : ↑s
hz : x < z
hz' : z < y
hz0 : ⊥ < ↑z
⊢ ↑z < ↑((↑y).unbot ⋯)
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithTop X)
⊢ DenselyOrdered ↑s ↔ s.Subsingleton

Tactic:
have he : StrictAnti (WithTop.toDual.image s) :=
    WithTop.toDual.image_strictAnti _ (fun ⦃a b⦄ a ↦ a)
  rw [denselyOrdered_iff_of_strictAnti _ he, WithBot.denselyOrdered_set_iff_subsingleton,
    WithTop.toDual.injective.subsingleton_image_iff]

Goal state after:
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithTop X)
⊢ DenselyOrdered ↑s ↔ s.Subsingleton

Tactic:
by
  have he : StrictAnti (WithTop.toDual.image s) :=
    WithTop.toDual.image_strictAnti _ (fun ⦃a b⦄ a ↦ a)
  rw [denselyOrdered_iff_of_strictAnti _ he, WithBot.denselyOrdered_set_iff_subsingleton,
    WithTop.toDual.injective.subsingleton_image_iff]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
⊢ ↥(closure {x}) ≃*o ↥(closure {y})

Tactic:
have hxc : closure {x} = closure {x'} := by rcases max_cases x x⁻¹ <;> simp_all

Goal state after:
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : closure {x} = closure {x'}
⊢ ↥(closure {x}) ≃*o ↥(closure {y})
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
U : Set K
hU' : U.Nonempty
hU : ∀ x ∉ U, ∃ γ, U ⊆ {a | ↑γ ≤ v.restrict (a - x)}
⊢ 0 ∈ U ∨ ∃ γ, ¬γ = 0 ∧ U ⊆ ⇑v.restrict ⁻¹' Ici γ

Tactic:
refine (em _).imp_right fun h ↦ ?_

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
U : Set K
hU' : U.Nonempty
hU : ∀ x ∉ U, ∃ γ, U ⊆ {a | ↑γ ≤ v.restrict (a - x)}
h : 0 ∉ U
⊢ ∃ γ, ¬γ = 0 ∧ U ⊆ ⇑v.restrict ⁻¹' Ici γ