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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ W.c₄ = -48 * W.a₄

Tactic:
c₄,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ W.b₂ ^ 2 - 24 * W.b₄ = -48 * W.a₄
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: case a₂
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
ha₁ : W.a₁ = 0
⊢ (W.toCharTwoJEqZeroNF • W).a₂ = 0

Tactic:
simp_rw [toCharTwoJEqZeroNF, variableChange_a₂, inv_one, Units.val_one]

Goal state after:
case a₂
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
ha₁ : W.a₁ = 0
⊢ 1 ^ 2 * (W.a₂ - 0 * W.a₁ + 3 * W.a₂ - 0 ^ 2) = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ (u : R) {P : Fin 3 → R}, W'.Equation P → W'.Equation (u • P)
h : W'.Equation (u • P)
⊢ W'.Equation P

Tactic:
convert! hP (↑hu.unit⁻¹) h; rw [smul_smul, hu.val_inv_mul, one_smul]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P) W'.polynomialX = W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4)

Tactic:
polynomialX_eq

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P) (C W'.a₁ * Y * Z - (C 3 * X ^ 2 + C (2 * W'.a₂) * X * Z ^ 2 + C W'.a₄ * Z ^ 4)) =
    W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℤ
h : ↑n ≠ 0
⊢ W.preΨ n ≠ 0

Tactic:
by
  induction n using Int.negInduction with
  | nat n => simpa only [preΨ_ofNat] using W.preΨ'_ne_zero <| by exact_mod_cast h
  | neg ih n => simpa only [preΨ_neg, neg_ne_zero]
        using ih n <| neg_ne_zero.mp <| by exact_mod_cast h

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.neg P = P z • ![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]

Tactic:
rw [neg, smul_fin3]
  simp only [fin3_def_ext]
  rw [mul_div_cancel₀ _ <| pow_ne_zero 2 hPz, ← negY_of_Z_ne_zero hPz,
    mul_div_cancel₀ _ <| pow_ne_zero 3 hPz, mul_one]

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

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

Tactic:
add_of_not_equiv h

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : ¬P ≈ Q
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ (u * v) ^ 2 • W'.addXYZ P Q = (u * v) ^ 2 • W'.addXYZ P Q
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z = 0
⊢ W'.add P Q = -(Q x * P z) • P

Tactic:
rw [add_of_not_equiv <| not_equiv_of_Z_eq_zero_right hPz hQz, addXYZ_of_Z_eq_zero_right hQ hQz]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y : R
h : x <ᵥ y
⊢ y ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : R
h : x <ᵥ 0
⊢ False
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : ValuativeRel R
α : Type u_2
inst✝ : Mul α
f : R → ↥(posSubmonoid R) → α
hf : ∀ (x y : R) (t s : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t
hdist : ∀ (a b : R) (r s : ↥(posSubmonoid R)), f (a * b) (r * s) = f a r * f b s
a b : ValueGroupWithZero R
⊢ ValueGroupWithZero.lift f hf (a * b) = ValueGroupWithZero.lift f hf a * ValueGroupWithZero.lift f hf b

Tactic:
by
  induction a using ValueGroupWithZero.ind
  induction b using ValueGroupWithZero.ind
  simpa using hdist _ _ _ _

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).neg (⇑f ∘ P) = ⇑f ∘ W'.neg P

Tactic:
by
  simp only [neg, map_negY, comp_fin3]
  map_simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
s : Set R
x : R
⊢ s ∈ 𝓝 x ↔ ∃ γ, {y | v.restrict (y - x) < ↑γ} ⊆ s

Tactic:
by
  simp only [← nhds_translation_add_neg x, ← sub_eq_add_neg, preimage_ofPred_eq, true_and,
    ((hasBasis_nhds_zero R Γ₀).comap fun y ↦ y - x).mem_iff]

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_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x : R
s : Set R
⊢ (∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s) ↔ ∃ γ, {a | (valuation R) (a - x) < ↑γ} ⊆ s

Tactic:
refine ⟨fun ⟨r, hr⟩ ↦ ⟨r.mapEquiv (orderMonoidIso v).symm, ?_⟩,
    fun ⟨r, hr⟩ ↦ ⟨r.mapEquiv (orderMonoidIso v), ?_⟩⟩

Goal state after:
case refine_1
R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x : R
s : Set R
x✝ : ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s
r : (ofClass v).ValueGroup₀ˣ
hr : {z | v.restrict (z - x) < ↑r} ⊆ s
⊢ {a | (valuation R) (a - x) < ↑((Units.mapEquiv ↑(orderMonoidIso v).symm) r)} ⊆ s

case refine_2
R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x : R
s : Set R
x✝ : ∃ γ, {a | (valuation R) (a - x) < ↑γ} ⊆ s
r : (ValueGroupWithZero R)ˣ
hr : {a | (valuation R) (a - x) < ↑r} ⊆ s
⊢ {z | v.restrict (z - x) < ↑((Units.mapEquiv ↑(orderMonoidIso v)) r)} ⊆ s
Module: Mathlib.Topology.Algebra.GroupCompletion

Goal state before:
pp: M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : IsUniformAddGroup α
n : ℕ
a✝ : Completion α
a : α
⊢ ↑(↑n.succ • a) = ↑n • ↑a + ↑a

Tactic:
show (n.succ : ℤ) • a = (n : ℤ) • a + a from
            SubNegMonoid.zsmul_succ' n a,

Goal state after:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : IsUniformAddGroup α
n : ℕ
a✝ : Completion α
a : α
⊢ ↑(↑n • a + a) = ↑n • ↑a + ↑a
Module: Mathlib.Topology.Algebra.GroupCompletion

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : IsUniformAddGroup β
x : Completion α
⊢ (completion 0 ⋯) x = 0 x

Tactic:
refine Completion.induction_on x ?_ ?_

Goal state after:
case refine_1
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : IsUniformAddGroup β
x : Completion α
⊢ IsClosed {a | (completion 0 ⋯) a = 0 a}

case refine_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : IsUniformAddGroup β
x : Completion α
⊢ ∀ (a : α), (completion 0 ⋯) ↑a = 0 ↑a
Module: Mathlib.Topology.Algebra.GroupCompletion

Goal state before:
pp: α : 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 α
⊢ ((f + g).completion ⋯) x = (f.completion hf + g.completion hg) x

Tactic:
refine Completion.induction_on x ?_ ?_

Goal state after:
case refine_1
α : 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 α
⊢ IsClosed {a | ((f + g).completion ⋯) a = (f.completion hf + g.completion hg) a}

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
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x✝¹ x✝ : ValueGroupWithZero R
⊢ ∀ (a b a_1 : R) (b_1 : 0 <ᵥ a_1) (a_2 : R) (b_2 : 0 <ᵥ a_2),
    ((if h : (ofClass v) b = 0 then 0
        else
          if h : (ofClass v) a = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) a) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) b) ⋯, ⋯⟩) /
        if h : (ofClass v) a_2 = 0 then 0
        else
          if h : (ofClass v) a_1 = 0 then 0
          else ↑⟨Units.mk0 ((ofClass v) a_1) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) a_2) ⋯, ⋯⟩) =
      ((if h : (ofClass v) a = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) a) h, ⋯⟩) /
          if h : (ofClass v) a_1 = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) a_1) ⋯, ⋯⟩) *
        ((if h : (ofClass v) b = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) b) h, ⋯⟩) /
          if h : (ofClass v) a_2 = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) a_2) ⋯, ⋯⟩)

Tactic:
intro x y z hz w hw

Goal state after:
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
⊢ ((if h : (ofClass v) y = 0 then 0
      else if h : (ofClass v) x = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩) /
      if h : (ofClass v) w = 0 then 0
      else if h : (ofClass v) z = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩) =
    ((if h : (ofClass v) x = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) x) h, ⋯⟩) /
        if h : (ofClass v) z = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩) *
      ((if h : (ofClass v) y = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) y) h, ⋯⟩) /
        if h : (ofClass v) w = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩)
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
⊢ Relator.LiftFun (⇑(inseparableSetoid α)) (⇑(Submodule.quotientRel ⊥.closure)) id id

Tactic:
rw [inseparableSetoid_ring]; exact fun _ _ ↦ id

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

Goal state before:
pp: α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
⊢ Relator.LiftFun (⇑(Submodule.quotientRel ⊥.closure)) (⇑(inseparableSetoid α)) id id

Tactic:
rw [inseparableSetoid_ring]; exact fun _ _ ↦ id

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

Goal state before:
pp: K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : IsTopologicalDivisionRing L
inst✝¹ : T0Space L
inst✝ : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : F.NeBot
x : L
hx : F ≤ 𝓝 x
⊢ x ≠ 0

Tactic:
rintro rfl

Goal state after:
K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : IsTopologicalDivisionRing L
inst✝¹ : T0Space L
inst✝ : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : F.NeBot
hx : F ≤ 𝓝 0
⊢ False
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hπ : exp (-1) ∈ range ⇑v
⊢ generator v = Units.mk0 (exp (-1)) generator_eq_exp_neg_one_of_mem_range._proof_1

Tactic:
rw [← Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator]
  suffices Units.mk0 (exp (-1)) (by simp) = (Subgroup.genLTOne (valueGroup (.ofClass v))) by
    simp [← this]
  apply Subgroup.genLTOne_unique
  · exact compareOfLessAndEq_eq_lt.mp rfl
  · ext n
    simp_all only [Int.reduceNeg, exp_neg, Subgroup.mem_zpowers_iff, mem_valueGroup_iff_of_comm,
      ne_eq]
    refine ⟨fun ⟨k, h⟩ ↦ ?_ , fun _ ↦ ⟨-WithZero.log n, by aesop⟩⟩
    rw [← h]
    have ⟨π, hπ⟩ := hπ
    cases k with
    | ofNat n => refine ⟨1, ?_, π ^ n, ?_⟩ <;> simp [hπ]
    | negSucc n => refine ⟨π ^ (n + 1), ?_, 1, ?_⟩ <;> simp [hπ, Int.negSucc_eq, mul_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).dblZ (⇑f ∘ P) = f (W'.dblZ P)

Tactic:
simp only [dblZ, negY]

Goal state after:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ (⇑f ∘ P) z * ((⇑f ∘ P) y - (-(⇑f ∘ P) y - (W'.map f).a₁ * (⇑f ∘ P) x * (⇑f ∘ P) z - (W'.map f).a₃ * (⇑f ∘ P) z ^ 3)) =
    f (P z * (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)))
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case neg
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
⊢ Submodule.IsPrincipal P

Tactic:
let π : Uniformizer v := Nonempty.some (by infer_instance)
    obtain ⟨x, ⟨hx_mem, hx₀⟩⟩ := Submodule.exists_mem_ne_zero_of_ne_bot h_ne_bot
    obtain ⟨n, ⟨u, hu⟩⟩ := exists_pow_Uniformizer hx₀ π
    by_cases hn : n = 0
    · rw [← Subring.coe_mul, hn, pow_zero, one_mul, SetLike.coe_eq_coe] at hu
      refine (hP.ne_top (Ideal.eq_top_of_isUnit_mem P hx_mem ?_)).elim
      simp only [hu, Units.isUnit]
    · rw [← Subring.coe_mul, SetLike.coe_eq_coe] at hu
      rw [hu, Ideal.mul_unit_mem_iff_mem P u.isUnit,
        IsPrime.pow_mem_iff_mem hP _ (pos_iff_ne_zero.mpr hn),
        ← Ideal.span_singleton_le_iff_mem] at hx_mem
      replace hx_mem := π.is_generator ▸ hx_mem
      rw [← Ideal.IsMaximal.eq_of_le (IsLocalRing.maximalIdeal.isMaximal K₀) hP.ne_top hx_mem]
      exact ⟨π.1, π.is_generator⟩

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 Γ₀'
h : v.IsEquiv w
hcomp : WithVal.congr v w (RingEquiv.refl R) = WithVal.congr v w (RingEquiv.refl R)
h1 : UniformContinuous ⇑(equiv v)
⊢ UniformContinuous ⇑(WithVal.congr v w (RingEquiv.refl R))

Tactic:
have h2 := IsEquiv.uniformContinuous_equiv_symm (hval := Valued.mk' v) rfl h

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 Γ₀'
h : v.IsEquiv w
hcomp : WithVal.congr v w (RingEquiv.refl R) = WithVal.congr v w (RingEquiv.refl R)
h1 : UniformContinuous ⇑(equiv v)
h2 : UniformContinuous ⇑(equiv w).symm
⊢ UniformContinuous ⇑(WithVal.congr v w (RingEquiv.refl R))
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
⊢ False

Tactic:
have hz0 : (⊥ : WithBot X) < z := by simp [(Subtype.coe_lt_coe.mpr hz).trans_le']

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
⊢ False
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_3
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_1 y_1 : ↥(closure {x})),
    { toFun := fun x_2 ↦ ⟨1, ⋯⟩, invFun := fun x_2 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun (x_1 * y_1) =
      { toFun := fun x_2 ↦ ⟨1, ⋯⟩, invFun := fun x_2 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun x_1 *
        { toFun := fun x_2 ↦ ⟨1, ⋯⟩, invFun := fun x_2 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun y_1

Tactic:
intros
      simp

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 Γ₀
U : Set K
hU' : U.Nonempty
hU : ∀ x ∉ U, ∃ γ, U ⊆ {a | ↑γ ≤ v.restrict (a - x)}
h✝ : 0 ∉ U
γ : (ofClass v).ValueGroup₀ˣ
h : U ⊆ {a | ↑γ ≤ v.restrict a}
⊢ ∃ γ, ¬γ = 0 ∧ U ⊆ ⇑v.restrict ⁻¹' Ici γ

Tactic:
refine ⟨γ.1, γ.ne_zero, h.trans ?_⟩

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
γ : (ofClass v).ValueGroup₀ˣ
h : U ⊆ {a | ↑γ ≤ v.restrict a}
⊢ {a | ↑γ ≤ v.restrict a} ⊆ ⇑v.restrict ⁻¹' Ici ↑γ
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y | y ∈ closure {b ^ n} ∧ 1 < y} b
this✝ : closure {b ^ n} = closure {b}
this : (∃ n_1, (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
⊢ m * n = 1

Tactic:
rw [← zpow_right_inj this.right, zpow_mul', hm, zpow_one]

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₀ : 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
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
H : y₀ * x₀ = ↑z₀
⊢ z₀ ≠ 0

Tactic:
rintro rfl

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
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
y₀ : hat K
y₀_in : y₀ ∈ V'
H : y₀ * x₀ = ↑0
⊢ False
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 * extension y)

Tactic:
rw [embedding_strictMono.injective.eq_iff]

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)
⊢ extension (x * y) = extension x * extension 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
a : K
⊢ ∃ r, extensionValuation ↑a = v r

Tactic:
simp [extensionValuation_apply_coe a]

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 : hat K
h : x ≠ 0
hr : ∀ (r : K), embedding ((restrict₀ (ofClass v)) r) = v r
a b : (ofClass v).ValueGroup₀
⊢ embedding a = embedding b ↔ a = b

Tactic:
rw [embedding_strictMono.injective.eq_iff]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
⊢ ({x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ))

Tactic:
← wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete_of_ne_zero hg',

Goal state after:
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
⊢ ({x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2) ↔ {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsDiscreteValuationRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
W : WeierstrassCurve K
inst✝ : IsMinimal R W
⊢ HasGoodReduction R W ∨ HasMultiplicativeReduction R W ∨ HasAdditiveReduction R W

Tactic:
hasGoodReduction_iff,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsDiscreteValuationRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
W : WeierstrassCurve K
inst✝ : IsMinimal R W
⊢ IsMinimal R W ∧ (valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.Δ = 1 ∨
    HasMultiplicativeReduction R W ∨ HasAdditiveReduction R W
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case h₀.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ ¬(i, j).2 = n

Tactic:
rintro rfl

Goal state after:
case h₀.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + (i, j).2)
h2 : (i, j) ≠ (d, (i, j).2)
⊢ False
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case h₀.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (n, d)
⊢ ¬(i, j).1 = n

Tactic:
rintro rfl

Goal state after:
case h₀.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + (i, j).1)
h2 : (i, j) ≠ ((i, j).1, d)
⊢ False
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
hxy : v xy = embedding a * embedding b
hx : v x = embedding a
hy : v y = embedding b
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ↑⟨Units.mk0 (v xy) ⋯, ⋯⟩ = ↑⟨Units.mk0 (v x) ⋯, ⋯⟩ * ↑⟨Units.mk0 (v y) ⋯, ⋯⟩

Tactic:
simp only [← WithZero.coe_mul, MulMemClass.mk_mul_mk, WithZero.coe_inj, Subtype.mk.injEq]
          rw [← Units.mk0_mul]
          · ext
            simp [Units.val_mk0, hx, hy, hxy]
          · aesop

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : σ →₀ ℕ
a : R
⊢ (map f) ((monomial n) a) = (monomial n) (f a)

Tactic:
ext m

Goal state after:
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (coeff m) ((map f) ((monomial n) a)) = (coeff m) ((monomial n) (f a))