mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case pos.inr.refine_1
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
⊢ -y ≠ 0

pp: case pos.inr.refine_2
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
⊢ 0 < -y

Tactic:
·

Goal state after:
case pos.inr.refine_1
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
⊢ -y ≠ 0
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case pos.inr.refine_2
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
⊢ 0 < -y

Tactic:
·

Goal state after:
case pos.inr.refine_2
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
⊢ 0 < -y
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case neg
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 : ∃ x y, 0 < y ∧ ∀ (n : ℕ), n • y < x
⊢ Nonempty (G ≃+o ℤ)

Tactic:
·

Goal state after:
case neg
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 : ∃ x y, 0 < y ∧ ∀ (n : ℕ), n • y < x
⊢ Nonempty (G ≃+o ℤ)
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case hp
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)
⊢ IsClosed {x | extension (x.1 * x.2) = extension x.1 * extension x.2}

pp: case ih
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)
⊢ ∀ (a b : K), extension (↑a * ↑b) = extension ↑a * extension ↑b

Tactic:
·

Goal state after:
case hp
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)
⊢ IsClosed {x | extension (x.1 * x.2) = extension x.1 * extension x.2}
Module: Mathlib.GroupTheory.ArchimedeanDensely

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

Tactic:
·

Goal state after:
case mpr
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
⊢ Nonempty (G ≃+o ℤ) → {x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case ih
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)
⊢ ∀ (a b : K), extension (↑a * ↑b) = extension ↑a * extension ↑b

Tactic:
·

Goal state after:
case ih
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)
⊢ ∀ (a b : K), extension (↑a * ↑b) = extension ↑a * extension ↑b
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

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

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
⊢ ∃ C, IsIntegral R (C • W)
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:
·

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
⊢ MapsTo (fun x ↦ -x) {x | -g ≤ x} {x | x ≤ g}
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case hp
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)
⊢ IsClosed {x | extension (x.1 + x.2) ≤ extension x.1 ∨ extension (x.1 + x.2) ≤ extension x.2}

pp: case ih
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)
⊢ ∀ (a b : K), extension (↑a + ↑b) ≤ extension ↑a ∨ extension (↑a + ↑b) ≤ extension ↑b

Tactic:
·

Goal state after:
case hp
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)
⊢ IsClosed {x | extension (x.1 + x.2) ≤ extension x.1 ∨ extension (x.1 + x.2) ≤ extension x.2}
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:
·

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 ∈ {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:
·

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
⊢ MapsTo (fun x ↦ -x) {x | x ≤ g} {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:
·

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 ∈ {x | x ≤ g}, ∀ b ∈ {x | x ≤ g}, a > b → Function.onFun (fun x1 x2 ↦ x1 < x2) (fun x ↦ -x) a b
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case ih
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)
⊢ ∀ (a b : K), extension (↑a + ↑b) ≤ extension ↑a ∨ extension (↑a + ↑b) ≤ extension ↑b

Tactic:
·

Goal state after:
case ih
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)
⊢ ∀ (a b : K), extension (↑a + ↑b) ≤ extension ↑a ∨ extension (↑a + ↑b) ≤ extension ↑b
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ ∃ r, extensionValuation 0 = v r

pp: case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : hat K
h : x ≠ 0
⊢ ∃ r, extensionValuation x = v r

Tactic:
·

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ ∃ r, extensionValuation 0 = v r
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : hat K
h : x ≠ 0
⊢ ∃ r, extensionValuation x = v r

Tactic:
·

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : hat K
h : x ≠ 0
⊢ ∃ r, extensionValuation x = v r
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : hat K
h : x ≠ 0
⊢ IsClosed {b | ∃ r, extensionValuation b = v r}

Tactic:
·

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : hat K
h : x ≠ 0
⊢ IsClosed {b | ∃ r, extensionValuation b = v r}
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:
·

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
⊢ MapsTo (fun x ↦ x⁻¹) {x | g⁻¹ ≤ 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:
·

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 ∈ {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:
·

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
⊢ MapsTo (fun x ↦ x⁻¹) {x | x ≤ g} {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:
·

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 ∈ {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✝¹ : 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
f : G₀ˣ ≃*o Multiplicative ℤ
⊢ G₀ ≃* WithZero (Multiplicative ℤ)

pp: case refine_2
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
f : G₀ˣ ≃*o Multiplicative ℤ
⊢ ∀ {a b : G₀}, (MulEquiv.toEquiv ?refine_1).toFun a ≤ (MulEquiv.toEquiv ?refine_1).toFun b ↔ a ≤ b

pp: case refine_3
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
f : G₀ ≃*o WithZero (Multiplicative ℤ)
⊢ G₀ˣ ≃* Multiplicative ℤ

pp: case refine_4
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
f : G₀ ≃*o WithZero (Multiplicative ℤ)
⊢ ∀ {a b : G₀ˣ}, (MulEquiv.toEquiv ?refine_3).toFun a ≤ (MulEquiv.toEquiv ?refine_3).toFun b ↔ a ≤ b

Tactic:
·

Goal state after:
case refine_1
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
f : G₀ˣ ≃*o Multiplicative ℤ
⊢ G₀ ≃* WithZero (Multiplicative ℤ)
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
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
f : G₀ˣ ≃*o Multiplicative ℤ
⊢ ∀ {a b : G₀},
    (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun a ≤
        (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun b ↔
      a ≤ b

pp: case refine_3
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
f : G₀ ≃*o WithZero (Multiplicative ℤ)
⊢ G₀ˣ ≃* Multiplicative ℤ

pp: case refine_4
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
f : G₀ ≃*o WithZero (Multiplicative ℤ)
⊢ ∀ {a b : G₀ˣ}, (MulEquiv.toEquiv ?refine_3).toFun a ≤ (MulEquiv.toEquiv ?refine_3).toFun b ↔ a ≤ b

Tactic:
·

Goal state after:
case refine_2
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
f : G₀ˣ ≃*o Multiplicative ℤ
⊢ ∀ {a b : G₀},
    (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun a ≤
        (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun b ↔
      a ≤ b
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2.inl
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
f : G₀ˣ ≃*o Multiplicative ℤ
b : G₀
⊢ (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun 0 ≤
      (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun b ↔
    0 ≤ b

pp: case refine_2.inr
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
f : G₀ˣ ≃*o Multiplicative ℤ
a b : G₀
ha : a ≠ 0
⊢ (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun a ≤
      (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun b ↔
    a ≤ b

Tactic:
·

Goal state after:
case refine_2.inl
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
f : G₀ˣ ≃*o Multiplicative ℤ
b : G₀
⊢ (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun 0 ≤
      (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun b ↔
    0 ≤ b
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2.inr.inl
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
f : G₀ˣ ≃*o Multiplicative ℤ
a : G₀
ha : a ≠ 0
⊢ (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun a ≤
      (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun 0 ↔
    a ≤ 0

pp: case refine_2.inr.inr
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
f : G₀ˣ ≃*o Multiplicative ℤ
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun a ≤
      (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun b ↔
    a ≤ b

Tactic:
·

Goal state after:
case refine_2.inr.inl
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
f : G₀ˣ ≃*o Multiplicative ℤ
a : G₀
ha : a ≠ 0
⊢ (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun a ≤
      (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun 0 ↔
    a ≤ 0
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inl
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 < ↑γ}) ↔ γ₀ < ↑γ)
h : γ₀ = 0
⊢ x ∈ closure (Completion.coe' '' {x | v x < ↑γ}) ↔ x ∈ {x | extensionValuation x < ↑γ}

pp: case inr
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 < ↑γ}) ↔ γ₀ < ↑γ)
h : γ₀ ≠ 0
⊢ x ∈ closure (Completion.coe' '' {x | v x < ↑γ}) ↔ x ∈ {x | extensionValuation x < ↑γ}

Tactic:
·

Goal state after:
case inl
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 < ↑γ}) ↔ γ₀ < ↑γ)
h : γ₀ = 0
⊢ x ∈ closure (Completion.coe' '' {x | v x < ↑γ}) ↔ x ∈ {x | extensionValuation x < ↑γ}
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_3
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
f : G₀ ≃*o WithZero (Multiplicative ℤ)
⊢ G₀ˣ ≃* Multiplicative ℤ

pp: case refine_4
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
f : G₀ ≃*o WithZero (Multiplicative ℤ)
⊢ ∀ {a b : G₀ˣ}, (MulEquiv.toEquiv ?refine_3).toFun a ≤ (MulEquiv.toEquiv ?refine_3).toFun b ↔ a ≤ b

Tactic:
·

Goal state after:
case refine_3
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
f : G₀ ≃*o WithZero (Multiplicative ℤ)
⊢ G₀ˣ ≃* Multiplicative ℤ
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_4
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
f : G₀ ≃*o WithZero (Multiplicative ℤ)
⊢ ∀ {a b : G₀ˣ},
    (MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans ↑f)).toFun a ≤
        (MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans ↑f)).toFun b ↔
      a ≤ b

Tactic:
·

Goal state after:
case refine_4
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
f : G₀ ≃*o WithZero (Multiplicative ℤ)
⊢ ∀ {a b : G₀ˣ},
    (MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans ↑f)).toFun a ≤
        (MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans ↑f)).toFun b ↔
      a ≤ b