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

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

Tactic:
rw [Category.comp_id, Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left,
      reassoc_of% this, Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left,
      ← Over.comp_left_assoc, ← Comma.comp_hom, ← Functor.comp_map, Cocone.w]

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

Goal state before:
pp: C✝ : Type u_1
inst✝³ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝² : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst✝¹ : EffectiveEpiFamily Z fun i ↦ g i ≫ f i
inst✝ : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
i : I
⊢ f i ≫ EffectiveEpiFamily.desc Z (fun i ↦ g i ≫ f i) (fun i ↦ g i ≫ φ i) ⋯ = φ i

Tactic:
by
    rw [← cancel_epi (g i), ← assoc, EffectiveEpiFamily.fac _ (fun i => g i ≫ f i)]

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'
⊢ fst π (𝒰.f i) ≫ f = snd π (𝒰.f i) ≫ u ≫ Opens.ι ↑(↑i).2

Tactic:
simp [reassoc_of% hu, f']

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₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
x✝² x✝¹ c x✝ : Ideal W.CoordinateRing
⊢ x✝² ⊔ (x✝¹ ⊔ (c ⊔ x✝)) = x✝² ⊔ x✝ ⊔ x✝¹ ⊔ c

Tactic:
by rw [← sup_assoc, sup_comm c, sup_sup_sup_comm, ← sup_assoc]

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₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ (span {XClass W x₁} ⊔ (span {XClass W x₂} ⊔ span {(mk W) (Y - W.negPolynomial)})) *
      span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} =
    span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}

Tactic:
convert! top_mul (_ : Ideal W.CoordinateRing)

Goal state after:
case e'_2.e'_5
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ span {XClass W x₁} ⊔ (span {XClass W x₂} ⊔ span {(mk W) (Y - W.negPolynomial)}) = ⊤
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS' b c d (2 * (m + 3)) =
    preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2

Tactic:
show 2 * (m + 3) = 2 * m + 1 + 5 by rfl,

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS' b c d (2 * m + 1 + 5) =
    preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2
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)
inst✝ : c.pt.IsQuasiAffine
i : ↥c.pt → I
f : (x : ↥c.pt) → ↑Γ(D.obj (i x), ⊤)
hf : ∀ (x : ↥c.pt), IsAffineOpen ((D.obj (i x)).basicOpen (f x))
hi : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ (D.obj (i x)).basicOpen (f x)
σ : Finset ↥c.pt
hσ : ⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier = ⊤
σi : ↥c.pt → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi : ∀ (x : ↥c.pt), x ∈ (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))).carrier
j : I
fj : (i_1 : I) → i_1 ∈ Finset.image i σ → (j ⟶ i_1)
k : I
fkj : k ⟶ j
hk : D.map fkj ⁻¹ᵁ ⨆ k, D.map (fj (i (σi k)) ⋯) ⁻¹ᵁ (D.obj (i (σi k))).basicOpen (f (σi k)) = ⊤
x : ↥(D.obj k)
⊢ ∃ r, IsAffineOpen ((D.obj k).basicOpen r) ∧ x ∈ (D.obj k).basicOpen r

Tactic:
obtain ⟨y, hy⟩ := TopologicalSpace.Opens.mem_iSup.mp (hk.ge (Set.mem_univ x))

Goal state after:
I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
inst✝ : c.pt.IsQuasiAffine
i : ↥c.pt → I
f : (x : ↥c.pt) → ↑Γ(D.obj (i x), ⊤)
hf : ∀ (x : ↥c.pt), IsAffineOpen ((D.obj (i x)).basicOpen (f x))
hi : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ (D.obj (i x)).basicOpen (f x)
σ : Finset ↥c.pt
hσ : ⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier = ⊤
σi : ↥c.pt → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi : ∀ (x : ↥c.pt), x ∈ (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))).carrier
j : I
fj : (i_1 : I) → i_1 ∈ Finset.image i σ → (j ⟶ i_1)
k : I
fkj : k ⟶ j
hk : D.map fkj ⁻¹ᵁ ⨆ k, D.map (fj (i (σi k)) ⋯) ⁻¹ᵁ (D.obj (i (σi k))).basicOpen (f (σi k)) = ⊤
x : ↥(D.obj k)
y : ↥c.pt
hy : (D.map fkj) x ∈ D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y))
⊢ ∃ r, IsAffineOpen ((D.obj k).basicOpen r) ∧ x ∈ (D.obj k).basicOpen r
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), QuasiSeparatedSpace ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU' : IsCompact ↑U
hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U)
this : ∀ (j : Over i), CompactSpace ↥((opensDiagram D i U).obj j)
⊢ ∃ i_1 V, IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U

Tactic:
have (j : Over i) : QuasiSeparatedSpace ((opensDiagram D i U).obj j) :=
    (isQuasiSeparated_iff_quasiSeparatedSpace _ (D.map _ ⁻¹ᵁ _).2).mp (.of_quasiSeparatedSpace _)

Goal state after:
I : Type u
inst✝³ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU' : IsCompact ↑U
hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U)
this✝ : ∀ (j : Over i), CompactSpace ↥((opensDiagram D i U).obj j)
this : ∀ (j : Over i), QuasiSeparatedSpace ↥((opensDiagram D i U).obj j)
⊢ ∃ i_1 V, IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U
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), QuasiSeparatedSpace ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU' : IsCompact ↑U
hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U)
this✝ : ∀ (j : Over i), CompactSpace ↥((opensDiagram D i U).obj j)
this : ∀ (j : Over i), QuasiSeparatedSpace ↥((opensDiagram D i U).obj j)
⊢ ∃ i_1 V, IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U

Tactic:
have : IsAffine (opensCone D c i U).pt := hU

Goal state after:
I : Type u
inst✝³ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU' : IsCompact ↑U
hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U)
this✝¹ : ∀ (j : Over i), CompactSpace ↥((opensDiagram D i U).obj j)
this✝ : ∀ (j : Over i), QuasiSeparatedSpace ↥((opensDiagram D i U).obj j)
this : IsAffine (opensCone D c i U).pt
⊢ ∃ i_1 V, IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: 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
n : ℤ
⊢ f (normEDS b c d n) = normEDS (f b) (f c) (f d) n

Tactic:
by
  simp [normEDS, apply_ite f]

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

Goal state before:
pp: R : Type r
F : Type u
inst✝³ : CommRing R
inst✝² : Field F
W' : Affine R
inst✝¹ : DecidableEq F
inst✝ : Algebra R F
P : (W'⁄F).Point
⊢ (map (Algebra.ofId F F)) P = P

Tactic:
by
  cases P <;> rfl

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

Goal state before:
pp: R : Type r
S : Type s
F : Type u
K : Type v
L : Type w
inst✝¹⁷ : CommRing R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K
inst✝¹³ : Field L
W' : Affine R
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
P : (W'⁄F).Point
⊢ (map g) ((map f) P) = (map (g.comp f)) P

Tactic:
by
  cases P <;> rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.c₆ = -64 * W.a₂ ^ 3 + 288 * W.a₂ * W.a₄ - 864 * W.a₆

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

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ -(4 * W.a₂) ^ 3 + 36 * (4 * W.a₂) * (2 * W.a₄) - 216 * (4 * W.a₆) = -64 * W.a₂ ^ 3 + 288 * W.a₂ * W.a₄ - 864 * W.a₆
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
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:
· absurd hz
      apply vle_mul_cancel u.prop
      simpa using h₃.trans (mul_vle_mul_left hw v)

Goal state after:
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.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (∀ U ∈ ⋯.toRingFilterBasis.toAddGroupFilterBasis, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) ↔
    ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ

Tactic:
simp_rw [Valued.v.subgroups_basis.mem_addGroupFilterBasis_iff]

Goal state after:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (∀ (U : Set R), (∃ i, U = ↑(v.ltAddSubgroup ((Units.map ↑embedding) i))) → ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) ↔
    ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ y * ↑s ≤ᵥ 0 * ↑s

Tactic:
simpa using vle_trans h₂ (mul_vle_mul_left hx t)

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 : R
⊢ ∀ (x y : R) (t s : ↥(posSubmonoid R)),
    x * ↑t ≤ᵥ y * ↑s →
      y * ↑s ≤ᵥ x * ↑t →
        (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
          if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

Tactic:
intro x y t s h₁ h₂
    by_cases hx : x ≤ᵥ 0 <;> by_cases hy : y ≤ᵥ 0
    · simp [hx, hy]
    · absurd hy
      apply vle_mul_cancel s.prop
      simpa using vle_trans h₂ (mul_vle_mul_left hx t)
    · absurd hx
      apply vle_mul_cancel t.prop
      simpa using vle_trans h₁ (mul_vle_mul_left hy s)
    · simp only [dif_neg hx, dif_neg hy]
      apply ValueGroupWithZero.sound
      · grw [veq_mul_comm, veq_mul_comm _ x]
        simpa using h₂
      · grw [veq_mul_comm, veq_mul_comm _ y]
        simpa [mul_comm] using h₁

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 : ¬x ≤ᵥ 0
⊢ ValueGroupWithZero.mk x y * ValueGroupWithZero.mk ↑y ⟨x, h⟩ = ValueGroupWithZero.mk 1 1

Tactic:
ValueGroupWithZero.mk_mul_mk,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x : R
y : ↥(posSubmonoid R)
h : ¬x ≤ᵥ 0
⊢ ValueGroupWithZero.mk (x * ↑y) (y * ⟨x, h⟩) = ValueGroupWithZero.mk 1 1
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: K : Type u_2
inst✝¹ : DivisionRing K
inst✝ : ValuativeRel K
a b c : K
hc : c ≠ 0
⊢ a * c ≤ᵥ b / c * c ↔ a * c ≤ᵥ b

Tactic:
div_mul_cancel₀ _ (by lia)

Goal state after:
K : Type u_2
inst✝¹ : DivisionRing K
inst✝ : ValuativeRel K
a b c : K
hc : c ≠ 0
⊢ a * c ≤ᵥ b ↔ a * c ≤ᵥ b
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: K : Type u_2
inst✝¹ : DivisionRing K
inst✝ : ValuativeRel K
a b c : K
hc : c ≠ 0
⊢ a / c * c ≤ᵥ b * c ↔ a ≤ᵥ b * c

Tactic:
div_mul_cancel₀ _ (by lia)

Goal state after:
K : Type u_2
inst✝¹ : DivisionRing K
inst✝ : ValuativeRel K
a b c : K
hc : c ≠ 0
⊢ a ≤ᵥ b * c ↔ a ≤ᵥ b * c
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
⊢ W'.negAddY P Q * (P z * Q z) ^ 3 =
    (P y * Q z ^ 3 - Q y * P z ^ 3) * (W'.addX P Q * (P z * Q z) ^ 2 - P x * Q z ^ 2 * addZ P Q ^ 2) +
      P y * Q z ^ 3 * addZ P Q ^ 3

Tactic:
rw [negAddY, addX, addZ]
  ring1

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

Goal state before:
pp: Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝¹ : Ring A
v : Valuation A Γ
inst✝ : v.IsRankOneDiscrete
h1 : ∀ (x : A), v x ≠ 0 → v x = 1
⊢ ∀ (y : Γˣ) (x : A), (MonoidWithZeroHom.ofClass v) x = ↑y → ↑y = ↑1

Tactic:
intro y x

Goal state after:
Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝¹ : Ring A
v : Valuation A Γ
inst✝ : v.IsRankOneDiscrete
h1 : ∀ (x : A), v x ≠ 0 → v x = 1
y : Γˣ
x : A
⊢ (MonoidWithZeroHom.ofClass v) x = ↑y → ↑y = ↑1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ ![((u * v) ^ 2) ^ 2 * W'.addX P Q, ((u * v) ^ 2) ^ 3 * W'.addY P Q, (u * v) ^ 2 * addZ P Q] =
    ![((u * v) ^ 2) ^ 2 * W'.addX P Q, ((u * v) ^ 2) ^ 3 * W'.addY P Q, (u * v) ^ 2 * W'.addXYZ P Q z]

Tactic:
addXYZ_Z

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ ![((u * v) ^ 2) ^ 2 * W'.addX P Q, ((u * v) ^ 2) ^ 3 * W'.addY P Q, (u * v) ^ 2 * addZ P Q] =
    ![((u * v) ^ 2) ^ 2 * W'.addX P Q, ((u * v) ^ 2) ^ 3 * W'.addY P Q, (u * v) ^ 2 * addZ P Q]
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
⊢ b ∈ lowerBounds {y | y ∈ closure {b} ∧ 1 < y}

Tactic:
· intro x
      simp only [mem_closure_singleton, mem_ofPred_eq, and_imp, forall_exists_index]
      rintro k rfl hk
      rw [← zpow_one b, ← zpow_mul, one_mul, zpow_le_zpow_iff_right h, ← zero_add 1,
          ← Int.lt_iff_add_one_le]
      contrapose! hk
      rw [← Left.one_le_inv_iff, ← zpow_neg]
      exact one_le_zpow ha (by simp [hk])

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
i : ℕ := List.idxOf lmax l
hi : i < l.length
⊢ ∃ a, (valuation R K) a = lmax

Tactic:
use l₀[i]

Goal state after:
case h
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
i : ℕ := ⋯
hi : i < l.length
⊢ (valuation R K) l₀[i] = lmax
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff m) (φ * (monomial n) a) = if n ≤ m then (coeff (m - n)) φ * a else 0

Tactic:
have :
    ∀ p ∈ antidiagonal m,
      coeff (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 φ * coeff p.2 (monomial n a) ≠ 0 → p.2 = n :=
    fun p _ hp => eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hp)

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this : ∀ p ∈ antidiagonal m, (coeff p.1) φ * (coeff p.2) ((monomial n) a) ≠ 0 → p.2 = n
⊢ (coeff m) (φ * (monomial n) a) = if n ≤ m then (coeff (m - n)) φ * a else 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff n) (φ₁ * φ₂ * φ₃) = (coeff n) (φ₁ * (φ₂ * φ₃))

Tactic:
classical
  simp only [coeff_mul, Finset.sum_mul, Finset.mul_sum, Finset.sum_sigma']
  apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l + j), (l, j)⟩)
    (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩) <;> aesop (add simp [add_assoc, mul_assoc])

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
⊢ Ideal.span {r} ≠ 0

Tactic:
rw [Ne, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
⊢ ¬r = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : n ≤ m s
t : σ
hst : ¬s = t
⊢ (m - single s n + single s n) t = m t

Tactic:
simp [hst]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : R
| (MvPowerSeries.monomial e) r

Tactic:
← mul_one r

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : R
| (MvPowerSeries.monomial e) (r * 1)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case coe
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
a✝ : ℕ
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ↑a✝ → (coeff d) f = 0
⊢ ∀ (d : σ →₀ ℕ), (weight w) d < a✝ → (coeff d) f = 0

Tactic:
simpa only [ENat.some_eq_natCast, Nat.cast_lt] using h

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∈ s
m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝ ((truncFinset R s) ((monomial x) r)) = MvPolynomial.coeff m✝ ((MvPolynomial.monomial x) r)

Tactic:
grind [coeff_monomial, MvPolynomial.coeff_monomial]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f : MvPowerSeries σ R
⊢ weightedOrder w (-f) = weightedOrder w f

Tactic:
by_contra! h
  have : f = 0 := by simpa using (weightedOrder_add_of_weightedOrder_ne w h).symm
  simp [this] at h

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), (coeff n) p ∈ T
⊢ weightedOrder w (p.toSubring T hp) = weightedOrder w p

Tactic:
by
  refine eq_of_le_of_ge ?_ ?_
  · refine le_weightedOrder w fun d hd => by
      simp [coeff_eq_zero_of_lt_weightedOrder w hd, ← p.coeff_toSubring T hp]
  · refine le_weightedOrder w fun d hd => by
      exact_mod_cast (coeff_toSubring p T hp) ▸ (coeff_eq_zero_of_lt_weightedOrder w hd)

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑(degree d) < f.order
⊢ (coeff d) f = 0

Tactic:
rw [degree_eq_weight_one] at h
  exact coeff_eq_zero_of_lt_weightedOrder _ h

Goal state after:
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: a b✝ : ℕ∞
h : a ≠ ⊤ ∨ b✝ ≠ ⊤
b : ℕ
x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤
⊢ ∀ (n : ℕ), ∀ᶠ (a : ℕ∞) in 𝓝 ⊤, ↑b + ↑n < a

Tactic:
exact fun n ↦ lt_mem_nhds <| WithTop.coe_lt_top (b + n)

Goal state after: