mathlib-initiative/mathlib-tactics huggingface dataset:
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.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ ({ u := Units.mk0 u hu0, r := r, s := 0, t := 0 } • E).a₃ = E'.a₃

pp: case h.a₄
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ ({ u := Units.mk0 u hu0, r := r, s := 0, t := 0 } • E).a₄ = E'.a₄

pp: case h.a₆
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ ({ u := Units.mk0 u hu0, r := r, s := 0, t := 0 } • E).a₆ = E'.a₆

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

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

case h.a₆
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ ({ u := Units.mk0 u hu0, r := r, s := 0, t := 0 } • E).a₆ = E'.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case inr
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : E.IsElliptic
inst✝¹ : E'.IsElliptic
p : ℕ
inst✝ : CharP F p
heq : E.j = E'.j
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝⁴ : NeZero 2
this✝³ : NeZero 4
this✝² : NeZero 6
this✝¹ : Invertible 2 := invertibleOfNonzero hchar2
this✝ : Invertible 3 := invertibleOfNonzero hchar3
this : ∀ (E : WeierstrassCurve F) [inst : E.IsElliptic], E.j = E'.j → E.IsShortNF → ∃ C, C • E = E'
h✝ : ¬E.IsShortNF
⊢ ∃ C, C • E = E'

Tactic:
obtain ⟨C, hE⟩ := E.exists_variableChange_isShortNF
    rw [← variableChange_j E C] at heq
    obtain ⟨C', hC⟩ := this _ heq hE
    exact ⟨C' * C, by rwa [mul_smul]⟩

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

Goal state before:
pp: case succ.succ.left
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) := ⋯
n : ℕ
hd : (n + 1 + 1) ^ 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : (n + 1 + 1) ^ 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ ((X * W.preΨ' (n + 1 + 1) ^ 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
        W.preΨ' (n + 1 + 2) * W.preΨ' (n + 1) * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
    (n + 1 + 1) ^ 2

Tactic:
nth_rw 1 [← max_self <| (_ + _) ^ 2, hd, hd']

Goal state after:
case succ.succ.left
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1 + 1) ^ 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : (n + 1 + 1) ^ 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ ((X * W.preΨ' (n + 1 + 1) ^ 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
        W.preΨ' (n + 1 + 2) * W.preΨ' (n + 1) * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
    max (1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3)
      (expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_2
I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
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)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
i' : I
fi'i : i' ⟶ i
hi' : ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2
k : I
fki : k ⟶ i
ak : (j : ↥s) → ↑(D.map fki ⁻¹ᵁ 𝒱 j) ⟶ X
hak : ∀ (j : ↥s), ak j ≫ f = (D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ t.app k
hak' : ∀ (j : ↥s), c.π.app k ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j = (c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ a
l : I
flk : l ⟶ k
hl :
  ∀ (j₁ j₂ : ↥s),
    (D.obj l).homOfLE ⋯ ≫ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j₁ ≫ ak j₁ =
      (D.obj l).homOfLE ⋯ ≫ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j₂ ≫ ak j₂
h𝒲 : IsOpenCover fun k_1 ↦
  (Opens.comap (TopCat.Hom.hom (D.map flk).base)) ((Opens.comap (TopCat.Hom.hom (D.map fki).base)) (𝒱 k_1)) :=
  IsOpenCover.comap (IsOpenCover.comap h𝒱 (TopCat.Hom.hom (D.map fki).base)) (TopCat.Hom.hom (D.map flk).base)
𝒲 : (D.obj l).OpenCover := (D.obj l).openCoverOfIsOpenCover (fun x ↦ D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 x) h𝒲
F : D.obj l ⟶ X := Cover.glueMorphisms 𝒲 (fun j ↦ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j) ⋯
hF : ∀ (j : ↥s), (D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ F = D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j
⊢ F ≫ f = t.app l

Tactic:
· refine 𝒲.hom_ext _ _ fun j ↦ ?_
    simp [F, Cover.ι_glueMorphisms_assoc, hak]; rfl

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.neg (u • P) = u • W'.neg P

Tactic:
rw [neg, negY_smul]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ ![(u • P) x, u ^ 3 * W'.negY P, (u • P) z] = u • W'.neg P
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: case neg
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
⊢ (toNNReal he0) m = 1 ↔ m = 1

Tactic:
· refine ⟨fun h1 ↦ ?_, fun h1 ↦ h1 ▸ map_one _⟩
    rw [toNNReal_neg_apply he0 hm, zpow_eq_one_iff_right₀ _root_.zero_le he1, toAdd_eq_zero] at h1
    rw [← WithZero.coe_unzero hm, h1, coe_one]

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

Goal state before:
pp: case pos
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure[topologicalSpace] s) t
h₂ : Disjoint s (closure[topologicalSpace] t)
hs : 0 ∈ s
ht : 0 ∉ t
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
rwa [(isOpen_iff.2 (.inl ht)).nhdsSet_eq, disjoint_nhdsSet_principal]

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 Γ₀
inst✝² : TopologicalSpace R
v : Valuation R Γ₀
inst✝¹ : v.Compatible
inst✝ : IsTopologicalAddGroup R
H : ∀ {s : Set R}, s ∈ 𝓝 0 ↔ ∃ γ, {z | v.restrict z < ↑γ} ⊆ s
s : Set R
x : R
⊢ s ∈ 𝓝 x ↔ ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s

Tactic:
rw [← vadd_mem_nhds_vadd_iff (g := -x)]

Goal state after:
R : Type u_1
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : TopologicalSpace R
v : Valuation R Γ₀
inst✝¹ : v.Compatible
inst✝ : IsTopologicalAddGroup R
H : ∀ {s : Set R}, s ∈ 𝓝 0 ↔ ∃ γ, {z | v.restrict z < ↑γ} ⊆ s
s : Set R
x : R
⊢ -x +ᵥ s ∈ 𝓝 (-x +ᵥ x) ↔ ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case h₂
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
⊢ ↑⟨x, hx⟩ * ↑t ≤ᵥ y * ↑s

Tactic:
simpa [mul_comm] using h₁

Goal state after:
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✝¹ : AddCommGroup α
inst✝ : IsUniformAddGroup α
a b : Completion α
x y : α
⊢ ↑x + ↑y = ↑y + ↑x

Tactic:
by
        change (x : Completion α) + ↑y = ↑y + ↑x
        rw [← coe_add, ← coe_add, add_comm]

Goal state after:
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
x y z : R
⊢ ∀ (b : 0 <ᵥ z) (a : R) (b_1 : 0 <ᵥ a),
    ((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) a = 0 then 0
        else
          if h : (ofClass v) z = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) a) ⋯, ⋯⟩) =
      ((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) a = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) a) ⋯, ⋯⟩)

Tactic:
hz

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
⊢ ∀ (a : R) (b : 0 <ᵥ a),
    ((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) a = 0 then 0
        else
          if h : (ofClass v) z = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) a) ⋯, ⋯⟩) =
      ((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) a = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) a) ⋯, ⋯⟩)
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: case refine_2
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : IsUniformAddGroup A
inst✝³ : IsTopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion A
a : A
⊢ Completion.map (fun x ↦ r • x) ↑a = ↑((algebraMap R A) r) * ↑a

Tactic:
map_coe (uniformContinuous_const_smul r) a,

Goal state after:
case refine_2
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : IsUniformAddGroup A
inst✝³ : IsTopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion A
a : A
⊢ ↑(r • a) = ↑((algebraMap R A) r) * ↑a
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
x y : β
a b : α
⊢ ⋯.extend (⇑f) (i a + i b) = ⋯.extend (⇑f) (i a) + ⋯.extend (⇑f) (i b)

Tactic:
← i.map_add,

Goal state after:
case refine_2
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
x y : β
a b : α
⊢ ⋯.extend (⇑f) (i (a + b)) = ⋯.extend (⇑f) (i a) + ⋯.extend (⇑f) (i b)
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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x_ne : x ≠ 0
⊢ x * x⁻¹ = 1

Tactic:
by simp only [Inv.inv, if_neg x_ne, mul_hatInv_cancel x_ne]

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 Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
⊢ 0 < v π

Tactic:
by
  rw [IsUniformizer.iff] at hπ; simp [zero_lt_iff, ne_eq, hπ]

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

Goal state before:
pp: Γ : 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
g : Γˣ := Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup
hg : g = Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup
⊢ ↑g ∈ range ⇑(MonoidWithZeroHom.ofClass v) \ {0}

Tactic:
rw [← valueGroup_eq_range, hg]
    exact mem_image_of_mem Units.val (valueGroup (.ofClass v)).genLTOne_mem

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

Goal state before:
pp: Γ : 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
⊢ ∃ π, v.IsUniformizer ↑π

Tactic:
simp only [IsUniformizer.iff, Subtype.exists, mem_valuationSubring_iff, exists_prop]
  set g := (valueGroup (.ofClass v)).genLTOne with hg
  obtain ⟨⟨π, hπ⟩, hγ0⟩ : g.1 ∈ ((range (MonoidWithZeroHom.ofClass v)) \ {0}) := by
    rw [← valueGroup_eq_range, hg]
    exact mem_image_of_mem Units.val (valueGroup (.ofClass v)).genLTOne_mem
  use π
  simp only [MonoidWithZeroHom.coe_ofClass] at hπ
  rw [hπ, hg]
  exact ⟨le_of_lt (valueGroup (.ofClass v)).genLTOne_lt_one,
    by rw [valueGroup_genLTOne_eq_generator]⟩

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

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer ↑π₁
h2 : v.IsUniformizer ↑π₂
hval : v ((↑π₁)⁻¹ * ↑π₂) = 1
p : ↥v.integer := ⟨(↑π₁)⁻¹ * ↑π₂, ⋯⟩
hp : p = ⟨(↑π₁)⁻¹ * ↑π₂, ⋯⟩
⊢ Associated π₁ π₂

Tactic:
use ((Integers.isUnit_iff_valuation_eq_one (x := p) <| integer.integers v).mpr hval).unit

Goal state after:
case h
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer ↑π₁
h2 : v.IsUniformizer ↑π₂
hval : v ((↑π₁)⁻¹ * ↑π₂) = 1
p : ↥v.integer := ⋯
hp : p = ⟨(↑π₁)⁻¹ * ↑π₂, ⋯⟩
⊢ π₁ * ↑⋯.unit = π₂
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

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

Tactic:
rw [addXYZ, addX_of_Z_eq_zero_right hQz, addY_of_Z_eq_zero_right hQ hQz,
    addZ_of_Z_eq_zero_right hQz, smul_fin3]

Goal state after:
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 Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : x ∈ maximalIdeal ↥v.valuationSubring
hx₀ : ¬x = 0
⊢ x ∈ span {π.val}

Tactic:
· obtain ⟨n, ⟨u, hu⟩⟩ := exists_pow_Uniformizer hx₀ π
      rw [← Subring.coe_mul, Subtype.coe_inj] at hu
      have hn : Not (IsUnit x) := fun h ↦
        (maximalIdeal.isMaximal _).ne_top (eq_top_of_isUnit_mem _ hx h)
      replace hn : n ≠ 0 := fun h ↦ by
        simp only [hu, h, pow_zero, one_mul, Units.isUnit, not_true] at hn
      simp [Ideal.mem_span_singleton, hu, dvd_pow_self _ hn]

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

Goal state before:
pp: case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
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 = ↑γ
x : WithVal v
y : R := (equiv v) x
hy : toVal v y = x
hs0' : 0 < Valued.v.restrict (toVal v s)
h' : v.restrict.IsEquiv w.restrict
hx : Valued.v.restrict (x * toVal v s) < Valued.v.restrict (toVal v r)
⊢ v (y * s) < v r

Tactic:
restrict_lt_iff

Goal state after:
case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
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 = ↑γ
x : WithVal v
y : R := (equiv v) x
hy : toVal v y = x
hs0' : 0 < Valued.v.restrict (toVal v s)
h' : v.restrict.IsEquiv w.restrict
hx : Valued.v (x * toVal v s) < Valued.v (toVal v r)
⊢ v (y * s) < v r
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : 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
⊢ maximalIdeal ↥v.valuationSubring ≠ ⊥

Tactic:
by rw [ne_eq, ← isField_iff_maximalIdeal_eq]; exact valuationSubring_not_isField v

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 Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v x = v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ (v x)⁻¹ * v (y - x) * (v y)⁻¹ = v (y - x) * (v y * v y)⁻¹

Tactic:
rw [mul_assoc, mul_comm, key, mul_assoc, mul_inv_rev]

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 Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v x = v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ (v x)⁻¹ * v (y - x) * (v y)⁻¹ = v (y - x) * (v y * v y)⁻¹

Tactic:
by rw [mul_assoc, mul_comm, key, mul_assoc, mul_inv_rev]

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

Goal state before:
pp: case neg
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsDiscreteValuationRing A
x : A
hx : ¬x = 0
ϖ : A
hϖ : Irreducible ϖ
⊢ (maximalIdeal A).intValuation x = (ENat.recTopCoe 0 (fun x ↦ ↑(ofAdd ↑x)) ((addVal A) x))⁻¹

Tactic:
obtain ⟨n, u, rfl⟩ := eq_unit_mul_pow_irreducible hx hϖ

Goal state after:
case neg
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsDiscreteValuationRing A
ϖ : A
hϖ : Irreducible ϖ
n : ℕ
u : Aˣ
hx : ¬↑u * ϖ ^ n = 0
⊢ (maximalIdeal A).intValuation (↑u * ϖ ^ n) = (ENat.recTopCoe 0 (fun x ↦ ↑(ofAdd ↑x)) ((addVal A) (↑u * ϖ ^ n)))⁻¹
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 Γ₀
F : Filter K
hF : Cauchy F
h0 : 𝓝 0 ⊓ F = ⊥
U : Set K
U_in : U ∈ 𝓝 0
M : Set K
M_in : M ∈ F
H : U ∩ M = ∅
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
hU : {x | v.restrict x < ↑γ₀} ⊆ U
⊢ ∀ x ∈ M, ↑γ₀ ≤ v.restrict x

Tactic:
intro x xM

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
hF : Cauchy F
h0 : 𝓝 0 ⊓ F = ⊥
U : Set K
U_in : U ∈ 𝓝 0
M : Set K
M_in : M ∈ F
H : U ∩ M = ∅
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
hU : {x | v.restrict x < ↑γ₀} ⊆ U
x : K
xM : x ∈ M
⊢ ↑γ₀ ≤ v.restrict x
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
k : ℤ
hk : k ≤ 0
⊢ b ^ k ≤ 1

Tactic:
← Left.one_le_inv_iff,

Goal state after:
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
k : ℤ
hk : k ≤ 0
⊢ 1 ≤ (b ^ k)⁻¹
Module: Mathlib.Order.Northcott

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
h' : β → γ
inst✝² : Preorder β
inst✝¹ : LE γ
inst✝ : Northcott h
H : ∀ (c : γ), BddAbove (h' ⁻¹' {x | x ≤ c})
c : γ
⊢ {a | (h' ∘ h) a ≤ c}.Finite

Tactic:
obtain ⟨b, hb⟩ := bddAbove_def.mp (H c)
    exact (finite_le (h := h) b).subset <| by grind

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
⊢ (coeff m) (X ^ n) = if m = n then 1 else 0

Tactic:
X_pow_eq,

Goal state after:
R : Type u_1
inst✝ : Semiring R
m n : ℕ
⊢ (coeff m) ((monomial n) 1) = if m = n then 1 else 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∑ x ∈ (antidiagonal n).sigma fun a ↦ antidiagonal a.1, (coeff x.snd.1) φ₁ * (coeff x.snd.2) φ₂ * (coeff x.fst.2) φ₃ =
    ∑ x ∈ (antidiagonal n).sigma fun a ↦ antidiagonal a.2,
      (coeff x.fst.1) φ₁ * ((coeff x.snd.1) φ₂ * (coeff x.snd.2) φ₃)

Tactic:
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: