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

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

pp: case mp.inr
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
h : IsLeast {y | y ∈ closure {b ^ (-1)} ∧ 1 < y} b
this✝ : closure {b ^ (-1)} = closure {b}
this : (∃ n, (b ^ (-1)) ^ n = b) ∧ 1 < b
hm : (b ^ (-1)) ^ (-1) = b
⊢ |b ^ (-1)|ₘ = b ∧ 1 < b

Tactic:
<;>

Goal state after:
case mp.inl
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
h : IsLeast {y | y ∈ closure {b ^ 1} ∧ 1 < y} b
this✝ : closure {b ^ 1} = closure {b}
this : (∃ n, (b ^ 1) ^ n = b) ∧ 1 < b
hm : (b ^ 1) ^ 1 = b
⊢ |b ^ 1|ₘ = b ∧ 1 < b

case mp.inr
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
h : IsLeast {y | y ∈ closure {b ^ (-1)} ∧ 1 < y} b
this✝ : closure {b ^ (-1)} = closure {b}
this : (∃ n, (b ^ (-1)) ^ n = b) ∧ 1 < b
hm : (b ^ (-1)) ^ (-1) = b
⊢ |b ^ (-1)|ₘ = b ∧ 1 < b
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
⊢ (G ≃*o WithZero (Multiplicative ℤ)) → Gˣ ≃*o Multiplicative ℤ

pp: case refine_2
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
⊢ (Gˣ ≃*o Multiplicative ℤ) → G ≃*o WithZero (Multiplicative ℤ)

Tactic:
<;>

Goal state after:
case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
⊢ (G ≃*o WithZero (Multiplicative ℤ)) → Gˣ ≃*o Multiplicative ℤ

case refine_2
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
⊢ (Gˣ ≃*o Multiplicative ℤ) → G ≃*o WithZero (Multiplicative ℤ)
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case pos
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ b✝ : G
h✝¹ : a✝ = 0
h✝ : b✝ = 0
⊢ (map' ↑↑f) 0 ≤ (map' ↑↑f) 0 ↔ a✝ ≤ b✝

pp: case neg
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ b✝ : G
h✝¹ : a✝ = 0
h✝ : ¬b✝ = 0
⊢ (map' ↑↑f) 0 ≤ (map' ↑↑f) ↑(Units.mk0 b✝ h✝) ↔ a✝ ≤ b✝

pp: case pos
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ b✝ : G
h✝¹ : ¬a✝ = 0
h✝ : b✝ = 0
⊢ (map' ↑↑f) ↑(Units.mk0 a✝ h✝¹) ≤ (map' ↑↑f) 0 ↔ a✝ ≤ b✝

pp: case neg
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ b✝ : G
h✝¹ : ¬a✝ = 0
h✝ : ¬b✝ = 0
⊢ (map' ↑↑f) ↑(Units.mk0 a✝ h✝¹) ≤ (map' ↑↑f) ↑(Units.mk0 b✝ h✝) ↔ a✝ ≤ b✝

Tactic:
<;>

Goal state after:
case pos
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ b✝ : G
h✝¹ : a✝ = 0
h✝ : b✝ = 0
⊢ (map' ↑↑f) 0 ≤ (map' ↑↑f) 0 ↔ a✝ ≤ b✝

case neg
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ b✝ : G
h✝¹ : a✝ = 0
h✝ : ¬b✝ = 0
⊢ (map' ↑↑f) 0 ≤ (map' ↑↑f) ↑(Units.mk0 b✝ h✝) ↔ a✝ ≤ b✝

case pos
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ b✝ : G
h✝¹ : ¬a✝ = 0
h✝ : b✝ = 0
⊢ (map' ↑↑f) ↑(Units.mk0 a✝ h✝¹) ≤ (map' ↑↑f) 0 ↔ a✝ ≤ b✝

case neg
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ b✝ : G
h✝¹ : ¬a✝ = 0
h✝ : ¬b✝ = 0
⊢ (map' ↑↑f) ↑(Units.mk0 a✝ h✝¹) ≤ (map' ↑↑f) ↑(Units.mk0 b✝ h✝) ↔ a✝ ≤ b✝
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}

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

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}

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

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

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

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}

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
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}

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

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}

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_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}

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

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}

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.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
e : G ≃o Additive G := OrderIso.refl G
h : {x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ∀ a ∈ fun x ↦ instLEAdditive.1 (e g) x,
    ∀ b ∈ fun x ↦ instLEAdditive.1 (e g) x, a < b → Function.onFun (fun x1 x2 ↦ x1 < x2) (⇑e.symm) a b

pp: case refine_2
G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
h : {x | e g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
x✝ : G
⊢ x✝ ∈ {x | g ≤ x} → e x✝ ∈ {x | e g ≤ x}

pp: case refine_3
G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
h : {x | e g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ∀ a ∈ {x | g ≤ x}, ∀ b ∈ {x | g ≤ x}, a < b → Function.onFun (fun x1 x2 ↦ x1 < x2) (⇑e) a b

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
e : G ≃o Additive G := OrderIso.refl G
h : {x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ∀ a ∈ fun x ↦ instLEAdditive.1 (e g) x,
    ∀ b ∈ fun x ↦ instLEAdditive.1 (e g) x, a < b → Function.onFun (fun x1 x2 ↦ x1 < x2) (⇑e.symm) a b

case refine_2
G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
h : {x | e g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
x✝ : G
⊢ x✝ ∈ {x | g ≤ x} → e x✝ ∈ {x | e g ≤ x}

case refine_3
G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
h : {x | e g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ∀ a ∈ {x | g ≤ x}, ∀ b ∈ {x | g ≤ x}, a < b → Function.onFun (fun x1 x2 ↦ x1 < x2) (⇑e) 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}

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

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}

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_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}

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

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}

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.inr.refine_1
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 > x2
x : G₀
hx : x ≠ 0
⊢ 0 < g

pp: case refine_1.inr.refine_2
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 > x2
x : G₀
hx : x ≠ 0
⊢ 0 < x

Tactic:
<;>

Goal state after:
case refine_1.inr.refine_1
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 > x2
x : G₀
hx : x ≠ 0
⊢ 0 < g

case refine_1.inr.refine_2
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 > x2
x : G₀
hx : x ≠ 0
⊢ 0 < x
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : PartialOrder α
⊢ MulArchimedean (WithZero α) → MulArchimedean α

pp: case mpr
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : PartialOrder α
⊢ MulArchimedean α → MulArchimedean (WithZero α)

Tactic:
<;>

Goal state after:
case mp
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : PartialOrder α
⊢ MulArchimedean (WithZero α) → MulArchimedean α

case mpr
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : PartialOrder α
⊢ MulArchimedean α → MulArchimedean (WithZero α)
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mp
G₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero G₀
⊢ MulArchimedean G₀ˣ → MulArchimedean G₀

pp: case mpr
G₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero G₀
⊢ MulArchimedean G₀ → MulArchimedean G₀ˣ

Tactic:
<;>

Goal state after:
case mp
G₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero G₀
⊢ MulArchimedean G₀ˣ → MulArchimedean G₀

case mpr
G₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero G₀
⊢ MulArchimedean G₀ → MulArchimedean G₀ˣ
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : k - n = m
h₃ : k = m + n
⊢ a * b = a * b

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : k - n = m
h₃ : ¬k = m + n
⊢ a * b = 0

pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬k - n = m
h₃ : k = m + n
⊢ 0 * b = a * b

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬k - n = m
h₃ : ¬k = m + n
⊢ 0 * b = 0

pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : ¬n ≤ k
h₂ : k = m + n
⊢ 0 = a * b

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : ¬n ≤ k
h₂ : ¬k = m + n
⊢ 0 = 0

Tactic:
<;>

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : k - n = m
h₃ : k = m + n
⊢ a * b = a * b

case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : k - n = m
h₃ : ¬k = m + n
⊢ a * b = 0

case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬k - n = m
h₃ : k = m + n
⊢ 0 * b = a * b

case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬k - n = m
h₃ : ¬k = m + n
⊢ 0 * b = 0

case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : ¬n ≤ k
h₂ : k = m + n
⊢ 0 = a * b

case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : ¬n ≤ k
h₂ : ¬k = m + n
⊢ 0 = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case e'_2.mp
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (∀ m < n, (coeff m) φ = 0) → ∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff m) φ = 0

pp: case e'_2.mpr
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff m) φ = 0) → ∀ m < n, (coeff m) φ = 0

Tactic:
<;>

Goal state after:
case e'_2.mp
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (∀ m < n, (coeff m) φ = 0) → ∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff m) φ = 0

case e'_2.mpr
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff m) φ = 0) → ∀ m < n, (coeff m) φ = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (∀ m < 1, (coeff m) φ = 0) → (coeff 0) φ = 0

pp: case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (coeff 0) φ = 0 → ∀ m < 1, (coeff m) φ = 0

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (∀ m < 1, (coeff m) φ = 0) → (coeff 0) φ = 0

case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (coeff 0) φ = 0 → ∀ m < 1, (coeff m) φ = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
x : R⟦X⟧
n : ℕ
h : n = 0
⊢ (coeff n) ({ toFun := fun f ↦ mk fun n ↦ 0 ^ n * (coeff n) f, map_one' := ⋯, map_mul' := ⋯ } x) = constantCoeff x

pp: case neg
R : Type u_1
inst✝ : CommSemiring R
x : R⟦X⟧
n : ℕ
h : ¬n = 0
⊢ (coeff n) ({ toFun := fun f ↦ mk fun n ↦ 0 ^ n * (coeff n) f, map_one' := ⋯, map_mul' := ⋯ } x) = 0

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
x : R⟦X⟧
n : ℕ
h : n = 0
⊢ (coeff n) ({ toFun := fun f ↦ mk fun n ↦ 0 ^ n * (coeff n) f, map_one' := ⋯, map_mul' := ⋯ } x) = constantCoeff x

case neg
R : Type u_1
inst✝ : CommSemiring R
x : R⟦X⟧
n : ℕ
h : ¬n = 0
⊢ (coeff n) ({ toFun := fun f ↦ mk fun n ↦ 0 ^ n * (coeff n) f, map_one' := ⋯, map_mul' := ⋯ } x) = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : ↥(nonZeroDivisors R)
⊢ 0 < v.intValuation ↑x

Tactic:
v.intValuation_if_neg (nonZeroDivisors.coe_ne_zero x)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : ↥(nonZeroDivisors R)
⊢ 0 < exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑x})).factors))
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ (∀ (m : σ →₀ ℕ), m s < 1 → (coeff m) φ = 0) → ∀ (m : σ →₀ ℕ), m s = 0 → (coeff m) φ = 0

pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ (∀ (m : σ →₀ ℕ), m s = 0 → (coeff m) φ = 0) → ∀ (m : σ →₀ ℕ), m s < 1 → (coeff m) φ = 0

Tactic:
<;>

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ (∀ (m : σ →₀ ℕ), m s < 1 → (coeff m) φ = 0) → ∀ (m : σ →₀ ℕ), m s = 0 → (coeff m) φ = 0

case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ (∀ (m : σ →₀ ℕ), m s = 0 → (coeff m) φ = 0) → ∀ (m : σ →₀ ℕ), m s < 1 → (coeff m) φ = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case pos
A : Type u_2
inst✝ : CommRing A
a : A
n✝ : ℕ
h : n✝ = 1
⊢ a ^ n✝ * 1 = a * 1

pp: case neg
A : Type u_2
inst✝ : CommRing A
a : A
n✝ : ℕ
h : ¬n✝ = 1
⊢ a ^ n✝ * 0 = a * 0

Tactic:
<;>

Goal state after:
case pos
A : Type u_2
inst✝ : CommRing A
a : A
n✝ : ℕ
h : n✝ = 1
⊢ a ^ n✝ * 1 = a * 1

case neg
A : Type u_2
inst✝ : CommRing A
a : A
n✝ : ℕ
h : ¬n✝ = 1
⊢ a ^ n✝ * 0 = a * 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : n = m
h₂ : m = n
⊢ a = a

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : n = m
h₂ : ¬m = n
⊢ a = 0

pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : ¬n = m
h✝ : m = n
⊢ 0 = a

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : ¬n = m
h✝ : ¬m = n
⊢ 0 = 0

Tactic:
<;>

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : n = m
h₂ : m = n
⊢ a = a

case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : n = m
h₂ : ¬m = n
⊢ a = 0

case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : ¬n = m
h✝ : m = n
⊢ 0 = a

case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : ¬n = m
h✝ : ¬m = n
⊢ 0 = 0
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case mp
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Function.Surjective ⇑v → Function.Surjective ⇑v

pp: case mpr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Function.Surjective ⇑v → Function.Surjective ⇑v

Tactic:
<;>

Goal state after:
case mp
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Function.Surjective ⇑v → Function.Surjective ⇑v

case mpr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Function.Surjective ⇑v → Function.Surjective ⇑v
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x
⊢ ∃ n d, x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

pp: case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x⁻¹
⊢ ∃ n d, x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x
⊢ ∃ n d, x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x⁻¹
⊢ ∃ n d, x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d