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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
⊢ W.Nonsingular (W.add P Q)

Tactic:
by_cases hPz : P z = 0
  · by_cases hQz : Q z = 0
    · simp only [add_of_Z_eq_zero hP hQ hPz hQz,
        nonsingular_smul _ <| (isUnit_X_of_Z_eq_zero hP hPz).pow 2, nonsingular_zero]
    · simpa only [add_of_Z_eq_zero_left hP.left hPz hQz,
        nonsingular_smul _ <| (isUnit_X_of_Z_eq_zero hP hPz).mul <| Ne.isUnit hQz]
  · by_cases hQz : Q z = 0
    · simpa only [add_of_Z_eq_zero_right hQ.left hPz hQz,
        nonsingular_smul _ ((isUnit_X_of_Z_eq_zero hQ hQz).mul <| Ne.isUnit hPz).neg]
    · by_cases hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
      · by_cases hy : P y * Q z ^ 3 = Q y * P z ^ 3
        · simp only [add_of_Y_eq hPz hQz hxy.left hy hxy.right, nonsingular_smul _ <|
              isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, nonsingular_zero]
        · simp only [add_of_Y_ne hP.left hQ.left hPz hQz hxy.left hy,
            nonsingular_smul _ <| isUnit_addU_of_Y_ne hPz hQz hy, nonsingular_zero]
      · classical
        have := nonsingular_add_of_Z_ne_zero hP hQ hPz hQz hxy
        by_cases hx : P x * Q z ^ 2 = Q x * P z ^ 2
        · simpa only [add_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx,
            nonsingular_smul _ <| isUnit_dblZ_of_Y_ne' hP.left hQ.left hPz hx <| not_and.mp hxy hx]
        · simpa only [add_of_X_ne hP.left hQ.left hPz hQz hx,
            nonsingular_smul _ <| isUnit_addZ_of_X_ne hx]

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

Goal state before:
pp: F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z = 0
⊢ -((P y * Q z ^ 3 - Q y * 0 ^ 3) / 0) = 0

Tactic:
div_zero,

Goal state after:
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z = 0
⊢ -0 = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hQz : Q z = 0
⊢ -((P y * 0 ^ 3 - Q y * P z ^ 3) / 0) = 0

Tactic:
div_zero,

Goal state after:
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hQz : Q z = 0
⊢ -0 = 0
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
γx : Γ₀ˣ
Hx : v x = ↑γx
u : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu_def : u = Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu : embedding ↑u⁻¹ = ↑γx⁻¹
y : R
vy_lt : v y < embedding ↑(u⁻¹ * γ)
⊢ ↑γx * v y < ↑((Units.map ↑embedding) γ)

Tactic:
mul_comm

Goal state after:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
γx : Γ₀ˣ
Hx : v x = ↑γx
u : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu_def : u = Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu : embedding ↑u⁻¹ = ↑γx⁻¹
y : R
vy_lt : v y < embedding ↑(u⁻¹ * γ)
⊢ v y * ↑γx < ↑((Units.map ↑embedding) γ)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Jacobian R
W : Jacobian F
x✝² x✝¹ x✝ : W.Point
⊢ x✝² + x✝¹ + x✝ = x✝² + (x✝¹ + x✝)

Tactic:
classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, add_assoc]

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

Goal state before:
pp: R K : Type u
inst✝² : Ring R
inst✝¹ : DivisionRing K
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
s : Set R
⊢ s ∈ 𝓝 0 ↔ ∃ γ, {x | v.restrict x < ↑γ} ⊆ s

Tactic:
rw [Filter.hasBasis_iff.mp v.subgroups_basis.hasBasis_nhds_zero s]

Goal state after:
R K : Type u
inst✝² : Ring R
inst✝¹ : DivisionRing K
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
s : Set R
⊢ (∃ i, True ∧ ↑(v.ltAddSubgroup ((Units.map ↑embedding) i)) ⊆ s) ↔ ∃ γ, {x | v.restrict x < ↑γ} ⊆ s
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✝ a : R
x : ↥(posSubmonoid R)
ha : 0 < ValueGroupWithZero.mk a x
b : R
y : ↥(posSubmonoid R)
c : R
z : ↥(posSubmonoid R)
hbc : ValueGroupWithZero.mk b y < ValueGroupWithZero.mk c z
⊢ a * b * (↑x * ↑z) <ᵥ a * c * (↑x * ↑y)

Tactic:
grw [veq_mul_mul_mul_comm, veq_mul_mul_mul_comm _ c]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ a : R
x : ↥(posSubmonoid R)
ha : 0 < ValueGroupWithZero.mk a x
b : R
y : ↥(posSubmonoid R)
c : R
z : ↥(posSubmonoid R)
hbc : ValueGroupWithZero.mk b y < ValueGroupWithZero.mk c z
⊢ a * ↑x * (b * ↑z) <ᵥ a * ↑x * (c * ↑y)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₁ : Type u_3
Γ₂ : Type u_4
inst✝³ : LinearOrderedCommMonoidWithZero Γ₁
inst✝² : LinearOrderedCommMonoidWithZero Γ₂
v₁ : Valuation R Γ₁
v₂ : Valuation R Γ₂
inst✝¹ : v₁.Compatible
inst✝ : v₂.Compatible
x y : R
⊢ v₁ x ≤ v₁ y ↔ v₂ x ≤ v₂ y

Tactic:
simp_rw [← Valuation.Compatible.vle_iff_le]

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 y : R
r s : ↥(posSubmonoid R)
⊢ v x * v ↑r = v y * v ↑s →
    (restrict₀ (ofClass v)) x / (restrict₀ (ofClass v)) ↑s = (restrict₀ (ofClass v)) y / (restrict₀ (ofClass v)) ↑r

Tactic:
rw [div_eq_div_iff]

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 y : R
r s : ↥(posSubmonoid R)
⊢ v x * v ↑r = v y * v ↑s →
    (restrict₀ (ofClass v)) x * (restrict₀ (ofClass v)) ↑r = (restrict₀ (ofClass v)) y * (restrict₀ (ofClass v)) ↑s

case hb
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 y : R
r s : ↥(posSubmonoid R)
⊢ (restrict₀ (ofClass v)) ↑s ≠ 0

case hd
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 y : R
r s : ↥(posSubmonoid R)
⊢ (restrict₀ (ofClass v)) ↑r ≠ 0
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α : Type u_1
inst✝¹¹ : Ring α
inst✝¹⁰ : UniformSpace α
inst✝⁹ : IsTopologicalRing α
inst✝⁸ : IsUniformAddGroup α
β : Type u
inst✝⁷ : UniformSpace β
inst✝⁶ : Ring β
inst✝⁵ : IsUniformAddGroup β
inst✝⁴ : IsTopologicalRing β
f : α →+* β
hf : Continuous ⇑f
R : Type u_2
inst✝³ : CommRing R
inst✝² : UniformSpace R
inst✝¹ : IsUniformAddGroup R
inst✝ : IsTopologicalRing R
a✝ b✝ : Completion R
a b : R
⊢ ↑(a * b) = ↑(b * a)

Tactic:
mul_comm

Goal state after:
α : Type u_1
inst✝¹¹ : Ring α
inst✝¹⁰ : UniformSpace α
inst✝⁹ : IsTopologicalRing α
inst✝⁸ : IsUniformAddGroup α
β : Type u
inst✝⁷ : UniformSpace β
inst✝⁶ : Ring β
inst✝⁵ : IsUniformAddGroup β
inst✝⁴ : IsTopologicalRing β
f : α →+* β
hf : Continuous ⇑f
R : Type u_2
inst✝³ : CommRing R
inst✝² : UniformSpace R
inst✝¹ : IsUniformAddGroup R
inst✝ : IsTopologicalRing R
a✝ b✝ : Completion R
a b : R
⊢ ↑(b * a) = ↑(b * a)
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α : Type u_1
inst✝¹¹ : Ring α
inst✝¹⁰ : UniformSpace α
inst✝⁹ : IsTopologicalRing α
inst✝⁸ : IsUniformAddGroup α
β : Type u
inst✝⁷ : UniformSpace β
inst✝⁶ : Ring β
inst✝⁵ : IsUniformAddGroup β
inst✝⁴ : IsTopologicalRing β
f : α →+* β
hf : Continuous ⇑f
R : Type u_2
inst✝³ : CommRing R
inst✝² : UniformSpace R
inst✝¹ : IsUniformAddGroup R
inst✝ : IsTopologicalRing R
⊢ Algebra R (Completion R)

Tactic:
infer_instance

Goal state after:
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
a : A
⊢ (mapValueGroupWithZero A B) ((valuation A) a) = (valuation B) ((algebraMap A B) a)

Tactic:
by
  simp [valuation]

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
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
⊢ Nonempty v.Uniformizer

Tactic:
infer_instance

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).negDblY (⇑f ∘ P) = f (W'.negDblY P)

Tactic:
by
  simp only [negDblY, map_dblU, map_dblX, map_negY]
  simp

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

Goal state before:
pp: 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
this : Nontrivial ↥(MonoidWithZeroHom.ofClass (valuation K (maximalIdeal A))).valueGroup
⊢ (valuation K (maximalIdeal A)).IsRankOneDiscrete

Tactic:
infer_instance

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
⊢ v (x⁻¹ - y⁻¹) < ↑γ

Tactic:
have key : v x = v y := Valuation.map_eq_of_sub_lt v hyp2

Goal state after:
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
⊢ v (x⁻¹ - y⁻¹) < ↑γ
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 r s : K
y_ne : y ≠ 0
hr : r ≠ 0
hs : s ≠ 0
h : v (x - y) < min (v s / v r * (v y * v y)) (v y)
⊢ v (x⁻¹ - y⁻¹) * v r < v s

Tactic:
by
  have hr' : 0 < v r := by simp [zero_lt_iff, hr]
  let γ : Γ₀ˣ := .mk0 (v s / v r) (by simp [hs, hr])
  calc
    v (x⁻¹ - y⁻¹) * v r < γ * v r := by gcongr; exact Valuation.inversion_estimate v y_ne h
    _ = v s := div_mul_cancel₀ _ (by simpa)

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 Γ₀
⊢ IsTopologicalRing K

Tactic:
infer_instance

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 Γ₀
this : T2Space K
⊢ T0Space K

Tactic:
infer_instance

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

Goal state before:
pp: case refine_2
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝ : K
h : x✝ ∈ (valuation K (maximalIdeal A)).valuationSubring.toSubring
⊢ x✝ ∈ Subring.map (algebraMap A K) ⊤

Tactic:
· obtain ⟨y, rfl⟩ := exists_lift_of_le_one h
    rw [Subring.mem_map]
    exact ⟨y, mem_top _, rfl⟩

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}
⊢ {a | ↑γ ≤ v.restrict a} ⊆ ⇑v.restrict ⁻¹' Ici ↑γ

Tactic:
intro

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✝ : K
⊢ a✝ ∈ {a | ↑γ ≤ v.restrict a} → a✝ ∈ ⇑v.restrict ⁻¹' Ici ↑γ
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_1
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
this : ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃+o ℤ)
h : {x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ MapsTo (fun x ↦ x + g) {x | 0 ≤ x} {x | g ≤ x}

Tactic:
intro

Goal state after:
case refine_1
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
this : ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃+o ℤ)
h : {x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
x✝ : G
⊢ x✝ ∈ {x | 0 ≤ x} → (fun x ↦ x + g) x✝ ∈ {x | g ≤ x}
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
this : ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃+o ℤ)
h : {x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ∀ a ∈ {x | 0 ≤ x}, ∀ b ∈ {x | 0 ≤ x}, a < b → Function.onFun (fun x1 x2 ↦ x1 < x2) (fun x ↦ x + g) a b

Tactic:
intro

Goal state after:
case refine_2
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
this : ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃+o ℤ)
h : {x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
a✝ : G
⊢ a✝ ∈ {x | 0 ≤ x} → ∀ b ∈ {x | 0 ≤ x}, a✝ < b → Function.onFun (fun x1 x2 ↦ x1 < x2) (fun x ↦ x + g) a✝ b
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_3
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
this : ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃+o ℤ)
h : {x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ MapsTo (fun x ↦ x - g) {x | g ≤ x} {x | 0 ≤ x}

Tactic:
intro

Goal state after:
case refine_3
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
this : ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃+o ℤ)
h : {x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
x✝ : G
⊢ x✝ ∈ {x | g ≤ x} → (fun x ↦ x - g) x✝ ∈ {x | 0 ≤ x}
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_4
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
this : ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃+o ℤ)
h : {x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ∀ a ∈ {x | g ≤ x}, ∀ b ∈ {x | g ≤ x}, a < b → Function.onFun (fun x1 x2 ↦ x1 < x2) (fun x ↦ x - g) a b

Tactic:
intro

Goal state after:
case refine_4
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
this : ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃+o ℤ)
h : {x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
a✝ : G
⊢ a✝ ∈ {x | g ≤ x} → ∀ b ∈ {x | g ≤ x}, a✝ < b → Function.onFun (fun x1 x2 ↦ x1 < x2) (fun x ↦ x - g) a✝ b
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case pos.inr
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
this : ∀ (y : G), y ≠ 0 → 0 < y → False
hy' : y ≤ 0
⊢ False

pp: G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
hy' : 0 < y
⊢ False

Tactic:
· refine this (-y) ?_ ?_
        · simp [hy]
        · simp [lt_of_le_of_ne hy' hy]

Goal state after:
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
hy' : 0 < y
⊢ False
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_1
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : {x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ MapsTo (fun x ↦ -x) {x | -g ≤ x} {x | x ≤ g}

Tactic:
intro

Goal state after:
case refine_1
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : {x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2
x✝ : G
⊢ x✝ ∈ {x | -g ≤ x} → (fun x ↦ -x) x✝ ∈ {x | x ≤ g}
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : {x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ ∀ a ∈ {x | -g ≤ x}, ∀ b ∈ {x | -g ≤ x}, a < b → Function.onFun (fun x1 x2 ↦ x1 > x2) (fun x ↦ -x) a b

Tactic:
intro

Goal state after:
case refine_2
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : {x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2
a✝ : G
⊢ a✝ ∈ {x | -g ≤ x} → ∀ b ∈ {x | -g ≤ x}, a✝ < b → Function.onFun (fun x1 x2 ↦ x1 > x2) (fun x ↦ -x) a✝ b
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_3
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : {x | -g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ MapsTo (fun x ↦ -x) {x | x ≤ g} {x | -g ≤ x}

Tactic:
intro

Goal state after:
case refine_3
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : {x | -g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
x✝ : G
⊢ x✝ ∈ {x | x ≤ g} → (fun x ↦ -x) x✝ ∈ {x | -g ≤ x}
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_4
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : {x | -g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ∀ a ∈ {x | x ≤ g}, ∀ b ∈ {x | x ≤ g}, a > b → Function.onFun (fun x1 x2 ↦ x1 < x2) (fun x ↦ -x) a b

Tactic:
intro

Goal state after:
case refine_4
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : {x | -g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
a✝ : G
⊢ a✝ ∈ {x | x ≤ g} → ∀ b ∈ {x | x ≤ g}, a✝ > b → Function.onFun (fun x1 x2 ↦ x1 < x2) (fun x ↦ -x) a✝ b
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
h : {x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ MapsTo (fun x ↦ x⁻¹) {x | g⁻¹ ≤ x} {x | x ≤ g}

Tactic:
intro

Goal state after:
case refine_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
h : {x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2
x✝ : G
⊢ x✝ ∈ {x | g⁻¹ ≤ x} → (fun x ↦ x⁻¹) x✝ ∈ {x | x ≤ g}
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
h : {x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ ∀ a ∈ {x | g⁻¹ ≤ x}, ∀ b ∈ {x | g⁻¹ ≤ x}, a < b → Function.onFun (fun x1 x2 ↦ x1 > x2) (fun x ↦ x⁻¹) a b

Tactic:
intro

Goal state after:
case refine_2
G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
h : {x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2
a✝ : G
⊢ a✝ ∈ {x | g⁻¹ ≤ x} → ∀ b ∈ {x | g⁻¹ ≤ x}, a✝ < b → Function.onFun (fun x1 x2 ↦ x1 > x2) (fun x ↦ x⁻¹) a✝ b
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_3
G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
h : {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ MapsTo (fun x ↦ x⁻¹) {x | x ≤ g} {x | g⁻¹ ≤ x}

Tactic:
intro

Goal state after:
case refine_3
G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
h : {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
x✝ : G
⊢ x✝ ∈ {x | x ≤ g} → (fun x ↦ x⁻¹) x✝ ∈ {x | g⁻¹ ≤ x}
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_4
G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
h : {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ∀ a ∈ {x | x ≤ g}, ∀ b ∈ {x | x ≤ g}, a > b → Function.onFun (fun x1 x2 ↦ x1 < x2) (fun x ↦ x⁻¹) a b

Tactic:
intro

Goal state after:
case refine_4
G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
h : {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
a✝ : G
⊢ a✝ ∈ {x | x ≤ g} → ∀ b ∈ {x | x ≤ g}, a✝ > b → Function.onFun (fun x1 x2 ↦ x1 < x2) (fun x ↦ x⁻¹) a✝ b
Module: Mathlib.GroupTheory.ArchimedeanDensely

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

Tactic:
rw [this, LinearOrderedCommGroup.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete]

Goal state after:
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ Nonempty (G₀ˣ ≃*o Multiplicative ℤ) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ))
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
γ₀' : (ofClass v).ValueGroup₀ := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := extensionValuation x
hγ₀_def : γ₀ = extensionValuation x
heq : γ₀ = embedding γ₀'
this : γ₀ ≠ 0 → (x ∈ closure (Completion.coe' '' {x | v x < ↑γ}) ↔ γ₀ < ↑γ)
⊢ x ∈ closure (Completion.coe' '' {x | v x < ↑γ}) ↔ x ∈ {x | extensionValuation x < ↑γ}

Tactic:
by
    rcases eq_or_ne γ₀ 0 with h | h
    · simp only [(Valuation.zero_iff _).mp h, mem_ofPred_eq, Valuation.map_zero, Units.zero_lt,
        iff_true]
      apply subset_closure
      exact ⟨0, by simp only [mem_ofPred_eq, Valuation.map_zero, Units.zero_lt, true_and]; rfl⟩
    · exact this h

Goal state after: