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

Goal state before:
pp: case mpr
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X ⤏ Y
e : f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
⊢ IsOver S f

Tactic:
obtain ⟨f, rfl⟩ := PartialMap.toRationalMap_surjective f

Goal state after:
case mpr
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X.PartialMap Y
e : f.toRationalMap.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
⊢ IsOver S f.toRationalMap
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
⊢ f.toPartialMap.toRationalMap = f

Tactic:
obtain ⟨f, rfl⟩ := PartialMap.toRationalMap_surjective f

Goal state after:
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ f.toRationalMap.toPartialMap.toRationalMap = f.toRationalMap
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: ⊢ @UniversallyInjective = diagonal @Surjective

Tactic:
apply le_antisymm
  · intro X Y f hf
    refine ⟨fun x ↦ ⟨pullback.fst f f x, hf.1 _ _ _ (IsPullback.of_hasPullback f f) ?_⟩⟩
    rw [← Scheme.Hom.comp_apply, pullback.diagonal_fst]
    rfl
  · rw [← universally_eq_iff.mpr (inferInstance : IsStableUnderBaseChange (diagonal @Surjective)),
      universallyInjective_eq]
    apply universally_mono
    intro X Y f hf x₁ x₂ e
    obtain ⟨t, ht₁, ht₂⟩ := Scheme.Pullback.exists_preimage_pullback _ _ e
    obtain ⟨t, rfl⟩ := hf.1 t
    rw [← ht₁, ← ht₂, ← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, pullback.diagonal_fst,
      pullback.diagonal_snd]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case inr
I : Type u
inst✝⁹ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁸ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁷ : IsCofiltered I
inst✝⁶ : ∀ (i : I), IsAffine (D.obj i)
inst✝⁵ : IsAffine c.pt
i j : I
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝⁴ : IsAffine (Spec R)
S : CommRingCat
inst✝³ : IsAffine (Spec S)
a : D.obj i ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i ≫ a = c.π.app j ≫ b
φ : R ⟶ S
inst✝² : LocallyOfFiniteType (Spec.map φ)
ha : t.app i = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), IsAffine (D.obj i)]
    [IsAffine c.pt] (t : D ⟶ (Functor.const I).obj (Spec R)) (a : D.obj i ⟶ Spec S) (b : D.obj j ⟶ Spec S),
    c.π.app i ≫ a = c.π.app j ≫ b →
      t.app i = a ≫ Spec.map φ →
        t.app j = b ≫ Spec.map φ → (∃ D', D = D' ⋙ Scheme.Spec) → ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
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)
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b

Tactic:
have inst : IsAffine ((Cone.postcompose (asIso e).hom).obj c).pt := by
      dsimp; infer_instance

Goal state after:
case inr
I : Type u
inst✝¹⁰ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁸ : IsCofiltered I
inst✝⁷ : ∀ (i : I), IsAffine (D.obj i)
inst✝⁶ : IsAffine c.pt
i j : I
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝⁵ : IsAffine (Spec R)
S : CommRingCat
inst✝⁴ : IsAffine (Spec S)
a : D.obj i ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i ≫ a = c.π.app j ≫ b
φ : R ⟶ S
inst✝³ : LocallyOfFiniteType (Spec.map φ)
ha : t.app i = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), IsAffine (D.obj i)]
    [IsAffine c.pt] (t : D ⟶ (Functor.const I).obj (Spec R)) (a : D.obj i ⟶ Spec S) (b : D.obj j ⟶ Spec S),
    c.π.app i ≫ a = c.π.app j ≫ b →
      t.app i = a ≫ Spec.map φ →
        t.app j = b ≫ Spec.map φ → (∃ D', D = D' ⋙ Scheme.Spec) → ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
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)
inst : IsAffine ((Cone.postcompose (asIso e).hom).obj c).pt
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: case refine_2
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = U
V : Opens ((i : ι) × X i)
hc✝ : IsCompact V.carrier
heq : (fun p ↦ f p.fst p.snd) '' V.carrier = U
s : Set ι
t : (i : ι) → Set (X i)
hs : s.Finite
hc : ∀ (i : ι), IsCompact (t i)
heq' : s.sigma t = V.carrier
this : ∀ i ∈ s, IsOpen (t i)
⊢ ⋃ i ∈ s, f i '' t i = ⋃ i ∈ s, (fun p ↦ f p.fst p.snd) ∘ Sigma.mk i '' t i

Tactic:
Function.comp_apply

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.twoTorsionPolynomial = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }

Tactic:
rw [twoTorsionPolynomial]
  ext <;> dsimp
  · linear_combination CharP.cast_eq_zero R 3
  · linear_combination W.b₄ * CharP.cast_eq_zero R 3

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

Goal state before:
pp: case s
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ ↑C.u * (-C.s * ↑C.u⁻¹) + C.s = 0

Tactic:
linear_combination -C.s * C.u.inv_mul

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).a₆ = 0 ∧
      (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0) ↔
    (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).Nonsingular 0 0

Tactic:
← neg_ne_zero,

Goal state after:
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).a₆ = 0 ∧
      (-(W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0) ↔
    (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).Nonsingular 0 0
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
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:
Int.add_sub_cancel,

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) ^ 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
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:
Int.add_sub_cancel,

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) * preNormEDS b c d (↑n✝ + 1 + 1 + 1) ^ 3 * if Even (↑n✝ + 1 + 1) then 1 else b
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case some.some.mp
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂) → ¬some x₁ y₁ h✝¹ + some x₂ y₂ h✝ = 0

Tactic:
exact fun hxy => by simpa only [add_some hxy] using some_ne_zero _

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 3 ≠ 0
⊢ W.Ψ₃.coeff 4 ≠ 0

Tactic:
coeff_Ψ₃

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 3 ≠ 0
⊢ 3 ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 3 ≠ 0
⊢ W.Ψ₃.coeff 4 = 3

Tactic:
coeff_Ψ₃

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 3 ≠ 0
⊢ 3 = 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
P Q : W'.Point
⊢ P.sym2x Q ≠ 0

Tactic:
cases P <;> cases Q <;> simp [sym2x, xRep]

Goal state after:
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₁

Tactic:
simp_rw [variableChange_a₁, a₁_of_isCharThreeJNeZeroNF]

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
⊢ ↑(Units.mk0 u hu0)⁻¹ * (0 + 2 * 0) = 0
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₄

Tactic:
simp_rw [variableChange_a₄, a₁_of_isCharThreeJNeZeroNF, a₃_of_isCharThreeJNeZeroNF,
      a₄_of_isCharThreeJNeZeroNF]

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
⊢ ↑(Units.mk0 u hu0)⁻¹ ^ 4 * (0 - 0 * 0 + 2 * 0 * E.a₂ - (0 + 0 * 0) * 0 + 3 * 0 ^ 2 - 2 * 0 * 0) = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3
⊢ P y ≠ W'.negY P

Tactic:
have hy' : P y * Q z ^ 3 - W'.negY Q * P z ^ 3 = 0 :=
    (mul_eq_zero.mp <| Y_sub_Y_mul_Y_sub_negY hP hQ hx).resolve_left <| sub_ne_zero_of_ne hy

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3
hy' : P y * Q z ^ 3 - W'.negY Q * P z ^ 3 = 0
⊢ P y ≠ W'.negY P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
hx : ¬P x * Q z ^ 2 = Q x * P z ^ 2
⊢ ⟦W.add P Q⟧ =
    ⟦![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]⟧

Tactic:
add_of_X_ne hP hQ hPz hQz hx,

Goal state after:
case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
hx : ¬P x * Q z ^ 2 = Q x * P z ^ 2
⊢ ⟦addZ P Q •
        ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
            (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
          W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
            (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
          1]⟧ =
    ⟦![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]⟧
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
⊢ toAffine W (W.neg P) = -toAffine W P

Tactic:
by
  by_cases hPz : P z = 0
  · rw [neg_of_Z_eq_zero hP hPz,
      toAffine_smul _ ((isUnit_Y_of_Z_eq_zero hP hPz).div <| isUnit_X_of_Z_eq_zero hP hPz).neg,
      toAffine_zero, toAffine_of_Z_eq_zero hPz, Affine.Point.neg_zero]
  · rw [neg_of_Z_ne_zero hPz, toAffine_smul _ <| Ne.isUnit hPz, toAffine_some <|
        (nonsingular_smul _ <| Ne.isUnit hPz).mp <| neg_of_Z_ne_zero hPz ▸ nonsingular_neg hP,
      toAffine_of_Z_ne_zero hP hPz, Affine.Point.neg_some]

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

Goal state before:
pp: case left
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : r * ↑v ≤ᵥ s * ↑u
h2 : s * ↑u ≤ᵥ r * ↑v
h3 : s * ↑w ≤ᵥ t * ↑v
h4 : t * ↑v ≤ᵥ s * ↑w
this : r * ↑v * ↑w ≤ᵥ s * ↑w * ↑u
⊢ r * ↑w ≤ᵥ t * ↑u

Tactic:
have := vle_trans this (mul_vle_mul h3 (vle_refl _))

Goal state after:
case left
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : r * ↑v ≤ᵥ s * ↑u
h2 : s * ↑u ≤ᵥ r * ↑v
h3 : s * ↑w ≤ᵥ t * ↑v
h4 : t * ↑v ≤ᵥ s * ↑w
this✝ : r * ↑v * ↑w ≤ᵥ s * ↑w * ↑u
this : r * ↑v * ↑w ≤ᵥ t * ↑v * ↑u
⊢ r * ↑w ≤ᵥ t * ↑u
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ W.addX P Q =
    ((P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2 + W.a₁ * (P y * Q z ^ 3 - Q y * P z ^ 3) * P z * Q z * addZ P Q -
            W.a₂ * P z ^ 2 * Q z ^ 2 * addZ P Q ^ 2 -
          P x * Q z ^ 2 * addZ P Q ^ 2 -
        Q x * P z ^ 2 * addZ P Q ^ 2) /
      (P z * Q z) ^ 2

Tactic:
← addX_eq' hP hQ,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ W.addX P Q = W.addX P Q * (P z * Q z) ^ 2 / (P z * Q z) ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

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

Tactic:
by
  rw [addX, hPz]
  ring1

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

Goal state before:
pp: case neg.refine_2
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
h : y * ↑u ≤ᵥ w * ↑t
⊢ x * ↑v * ↑t * w ≤ᵥ z * ↑s * ↑t * w

Tactic:
calc x * v * t * w
          _ =ᵥ x * t * (w * v) := by grw [veq_mul_comm w, veq_mul_mul_mul_comm, mul_assoc]
          _ ≤ᵥ y * s * (z * u) := by gcongr
          _ =ᵥ y * u * (s * z) := by grw [veq_mul_comm z, veq_mul_mul_mul_comm, mul_assoc]
          _ ≤ᵥ w * t * (s * z) := by gcongr
          _ =ᵥ z * s * t * w := by grw [veq_mul_comm, veq_mul_comm _ z, veq_mul_comm w, ← mul_assoc]

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

Goal state before:
pp: case a
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 (Filter.comap coe' (𝓝 y))

pp: case a
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⁻¹
⊢ 𝓝 0 ⊓ Filter.comap coe' (𝓝 y) = ⊥

Tactic:
· have := isDenseInducing_coe.comap_nhds_neBot y
    apply cauchy_nhds.comap
    rw [Completion.comap_coe_eq_uniformity]

Goal state after:
case a
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⁻¹
⊢ 𝓝 0 ⊓ Filter.comap coe' (𝓝 y) = ⊥
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: case a
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⁻¹
⊢ 𝓝 0 ⊓ Filter.comap coe' (𝓝 y) = ⊥

Tactic:
· have eq_bot : 𝓝 (0 : hat K) ⊓ 𝓝 y = ⊥ := by
      by_contra h
      exact y_ne (eq_of_nhds_neBot <| neBot_iff.mpr h).symm
    rw [isDenseInducing_coe.nhds_eq_comap (0 : K), ← Filter.comap_inf]
    norm_cast
    rw [eq_bot]
    exact comap_bot

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x ↦ x * x.hatInv
c : K → hat K := fun x ↦ ↑x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' c '' {0}ᶜ)
z : K
z_ne : z ∈ {0}ᶜ
⊢ (fun x ↦ f (c x)) z = 1

Tactic:
rw [mem_compl_singleton_iff] at z_ne

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x ↦ x * x.hatInv
c : K → hat K := fun x ↦ ↑x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' c '' {0}ᶜ)
z : K
z_ne : z ≠ 0
⊢ (fun x ↦ f (c x)) z = 1
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Ring B
inst✝⁵ : ValuativeRel A
inst✝⁴ : ValuativeRel B
inst✝³ : Algebra A B
inst✝² : ValuativeExtension A B
Γ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ
w : Valuation B Γ
inst✝ : w.Compatible
⊢ (Valuation.comap (algebraMap A B) w).Compatible

Tactic:
by
  constructor
  simp [← vle_iff_vle (A := A) (B := B), Valuation.Compatible.vle_iff_le (v := w)]

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

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
x_ne : x ≠ 0
γ' : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hdef : γ' = Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
y : K
hy : y ∈ {y | v.restrict (y - 0) < ↑γ'}
⊢ y ∈ {k | v k < v x}

Tactic:
simp only [Valuation.restrict_lt_iff_lt_embedding, hdef, sub_zero, Units.val_mk0,
      mem_ofPred_eq, embedding_restrict₀] at hy
    simpa using hy

Goal state after:
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 y : K
h✝ : (valuation K (maximalIdeal A)) x = (valuation K (maximalIdeal A)) y
hx : ¬x = 0
hy : ¬y = 0
u : A
h : u ∈ ↑(IsUnit.submonoid A) ∧ (algebraMap A K) u = y / x
⊢ ∃ u, u • x = y

Tactic:
use IsUnit.unit h.1

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 y : K
h✝ : (valuation K (maximalIdeal A)) x = (valuation K (maximalIdeal A)) y
hx : ¬x = 0
hy : ¬y = 0
u : A
h : u ∈ ↑(IsUnit.submonoid A) ∧ (algebraMap A K) u = y / x
⊢ IsUnit.unit ⋯ • x = 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 Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
this : Tendsto (fun p ↦ p.1 * p.2⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
⊢ ∃ V' ∈ 𝓝 1, 0 ∉ V' ∧ ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V

Tactic:
rcases tendsto_prod_self_iff.mp this V V_in with ⟨U, U_in, hU⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
this : Tendsto (fun p ↦ p.1 * p.2⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').1 * (x, x').2⁻¹ ∈ V
⊢ ∃ V' ∈ 𝓝 1, 0 ∉ V' ∧ ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G✝ : Type u_1
inst✝⁷ : CommGroup G✝
inst✝⁶ : LinearOrder G✝
inst✝⁵ : IsOrderedMonoid G✝
inst✝⁴ : MulArchimedean G✝
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x : G
h : IsLeast {y | 0 < y} x
⊢ G ≃+o ℤ

Tactic:
by
  have : IsLeast {y : G | y ∈ (⊤ : AddSubgroup G) ∧ 0 < y} x := by simpa using h
  replace this := AddSubgroup.cyclic_of_min this
  let e : G ≃+o (⊤ : AddSubgroup G) := ⟨AddSubsemigroup.topEquiv.symm,
    (AddEquiv.strictMono_symm AddSubsemigroup.strictMono_topEquiv).le_iff_le⟩
  let e' : (⊤ : AddSubgroup G) ≃+o AddSubgroup.closure {x} :=
    ⟨AddEquiv.subsemigroupCongr (by simp [this]),
     (AddEquiv.strictMono_subsemigroupCongr _).le_iff_le⟩
  let g : (⊤ : AddSubgroup ℤ) ≃+o ℤ := ⟨AddSubsemigroup.topEquiv,
    (AddSubsemigroup.strictMono_topEquiv).le_iff_le⟩
  let g' : AddSubgroup.closure ({1} : Set ℤ) ≃+o (⊤ : AddSubgroup ℤ) :=
    ⟨(.subsemigroupCongr (by simp)),
     (AddEquiv.strictMono_subsemigroupCongr _).le_iff_le⟩
  let f := closure_equiv_closure x (1 : ℤ) (by simp [h.left.ne'])
  exact ((((e.trans e').trans f).trans g').trans g : G ≃+o ℤ)

Goal state after:
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 Γ₀
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (⇑embedding ∘ extension) (x + y) ≤ (⇑embedding ∘ extension) x ∨
    (⇑embedding ∘ extension) (x + y) ≤ (⇑embedding ∘ extension) y

Tactic:
Function.comp_apply

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ embedding (extension (x + y)) ≤ embedding (extension x) ∨ embedding (extension (x + y)) ≤ embedding (extension y)