-- 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:
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✝ ∈ Set.range (⇑v ∘ ⇑(algebraMap O F)) →
    (fun x => if hx : x ∈ MonoidHom.mrange v then ⟨x, hx⟩ else 1) x✝ ∈ {x | x ≤ 1}

Tactic:
simp only [Set.mem_range, Function.comp_apply, MonoidHom.mem_mrange, Set.mem_setOf_eq,
  forall_exists_index]

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✝ : Γ₀
⊢ ∀ (x : O), v ((algebraMap O F) x) = x✝ → (if h : ∃ x, v x = x✝ then ⟨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
hx : v x ≤ 1
⊢ ∃ y, v ((algebraMap O F) y) = v x

Tactic:
obtain ⟨y, rfl⟩ := hv.exists_of_le_one hx

Result:
case refine_1.mk.intro.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
y : O
hx : v ((algebraMap O F) y) ≤ 1
⊢ ∃ y_1, v ((algebraMap O F) y_1) = v ((algebraMap O F) y)

Proof state:
case refine_1.mk.intro.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
y : O
hx : v ((algebraMap O F) y) ≤ 1
⊢ ∃ y_1, v ((algebraMap O F) y_1) = v ((algebraMap O F) y)

Tactic:
exact ⟨y, by simp⟩

Result:
no goals

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
⊢ Set.MapsTo (fun x => if hx : x ∈ MonoidHom.mrange v then ⟨x, hx⟩ else 1) (Set.range (⇑v ∘ ⇑(algebraMap O F)))
    {x | x ≤ 1}

Tactic:
intro

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✝ : Γ₀
⊢ x✝ ∈ Set.range (⇑v ∘ ⇑(algebraMap O F)) →
    (fun x => if hx : x ∈ MonoidHom.mrange v then ⟨x, hx⟩ else 1) x✝ ∈ {x | x ≤ 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, ⋯⟩ ∈ {x | x ≤ 1} → ↑⟨v x, ⋯⟩ ∈ Set.range (⇑v ∘ ⇑(algebraMap O F))

Tactic:
simp only [← Subtype.coe_le_coe, OneMemClass.coe_one, Set.mem_setOf_eq, Set.mem_range,
  Function.comp_apply]

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 ≤ 1 → ∃ y, v ((algebraMap O F) y) = v x

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
h : (Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 => x1 > x2
y : O
hx : v ((algebraMap O F) y) ≤ 1
⊢ v ((algebraMap O F) y) = v ((algebraMap O F) y)

Tactic:
simp

Result:
no goals

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
h : (Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 => x1 > x2
⊢ ∀ a ∈ {x | x ≤ 1}, ∀ b ∈ {x | x ≤ 1}, a > b → ((fun x1 x2 => x1 > x2) on Subtype.val) a b

Tactic:
simp

Result:
no goals

Proof state:
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 fun x => if hx : x ∈ MonoidHom.mrange v then ⟨x, hx⟩ else 1) a b

Tactic:
simp [Function.onFun]

Result:
no goals

Proof state:
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)

Tactic:
exact fun x ↦ if hx : x ∈ MonoidHom.mrange v then ⟨x, hx⟩ else 1

Result:
no goals

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 : O
⊢ (if h : ∃ x_1, v x_1 = v ((algebraMap O F) x) then ⟨v ((algebraMap O F) x), ⋯⟩ else 1) ≤ 1

Tactic:
simp [← Subtype.coe_le_coe, hv.map_le_one]

Result:
no goals