-- Mathlib/RingTheory/Valuation/Archimedean.lean
lemma wellFounded_gt_on_v_iff_discrete_mrange [Nontrivial (MonoidHom.mrange v)ˣ]
    (hv : Integers v O) :
    WellFounded ((· > ·) on (v ∘ algebraMap O F)) ↔
      Nonempty (MonoidHom.mrange v ≃*o ℤₘ₀)

Proof state:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
⊢ ((Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 => x1 > x2) ↔
    {x | x ≤ 1}.WellFoundedOn fun x1 x2 => x1 > x2

Tactic:
refine ⟨fun h ↦ (h.mapsTo Subtype.val ?_).mono' (by simp), fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩

Result:
case refine_1
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : (Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 => x1 > x2
⊢ Set.MapsTo Subtype.val {x | x ≤ 1} (Set.range (⇑v ∘ ⇑(algebraMap O F)))

case refine_2
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : {x | x ≤ 1}.WellFoundedOn fun x1 x2 => x1 > x2
⊢ Γ₀ → ↥(MonoidHom.mrange v)

case refine_3
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : {x | x ≤ 1}.WellFoundedOn fun x1 x2 => x1 > x2
⊢ Set.MapsTo ?refine_2 (Set.range (⇑v ∘ ⇑(algebraMap O F))) {x | x ≤ 1}

case refine_4
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : {x | x ≤ 1}.WellFoundedOn fun x1 x2 => x1 > x2
⊢ ∀ a ∈ Set.range (⇑v ∘ ⇑(algebraMap O F)),
    ∀ b ∈ Set.range (⇑v ∘ ⇑(algebraMap O F)), a > b → ((fun x1 x2 => x1 > x2) on ?refine_2) a b

Proof state:
case refine_3
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : {x | x ≤ 1}.WellFoundedOn fun x1 x2 => x1 > x2
x✝ : Γ₀
⊢ ∀ (x : O), v ((algebraMap O F) x) = x✝ → (if h : ∃ x, v x = x✝ then ⟨x✝, ⋯⟩ else 1) ≤ 1

Tactic:
rintro x rfl

Result:
case refine_3
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : {x | x ≤ 1}.WellFoundedOn fun x1 x2 => x1 > x2
x : O
⊢ (if h : ∃ x_1, v x_1 = v ((algebraMap O F) x) then ⟨v ((algebraMap O F) x), ⋯⟩ else 1) ≤ 1

Proof state:
case refine_1.mk.intro
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : (Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 => x1 > x2
x : F
⊢ v x ≤ 1 → ∃ y, v ((algebraMap O F) y) = v x

Tactic:
intro hx

Result:
case refine_1.mk.intro
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : (Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 => x1 > x2
x : F
hx : v x ≤ 1
⊢ ∃ y, v ((algebraMap O F) y) = v x

Proof state:
case refine_1
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : (Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 => x1 > x2
⊢ Set.MapsTo Subtype.val {x | x ≤ 1} (Set.range (⇑v ∘ ⇑(algebraMap O F)))

Tactic:
rintro ⟨_, x, rfl⟩

Result:
case refine_1.mk.intro
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : (Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 => x1 > x2
x : F
⊢ ⟨v x, ⋯⟩ ∈ {x | x ≤ 1} → ↑⟨v x, ⋯⟩ ∈ Set.range (⇑v ∘ ⇑(algebraMap O F))

Proof state:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
⊢ WellFounded ((fun x1 x2 => x1 > x2) on ⇑v ∘ ⇑(algebraMap O F)) ↔ Nonempty (↥(MonoidHom.mrange v) ≃*o ℤₘ₀)

Tactic:
rw [← LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero
  one_ne_zero, ← Set.wellFoundedOn_range]

Result:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
⊢ ((Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 => x1 > x2) ↔
    {x | x ≤ 1}.WellFoundedOn fun x1 x2 => x1 > x2