-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Archimedean (goal)
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
refine_1 :
  ∀
    (h :
      Set.WellFoundedOn
        (Set.range.{u_2, u_3 + 1} (ι := O)
          (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
        fun (x1 x2 : Γ₀) ↦ x1 > x2),
    Set.MapsTo.{u_2, u_2} (α := ↥(MonoidHom.mrange v))
      (Subtype.val (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x))
      {x : ↥(MonoidHom.mrange v) | x ≤ 1}
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
refine_2 :
  (h : Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2) →
    Γ₀ → ↥(MonoidHom.mrange v)
refine_3 :
  ∀ (h : Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2),
    Set.MapsTo (β := ↥(MonoidHom.mrange v))
      (fun (x : Γ₀) ↦
        if hx : Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x then
          Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x) x hx
        else 1)
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      {x : ↥(MonoidHom.mrange v) | x ≤ 1}
⊢ (Set.WellFoundedOn
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      fun (x1 x2 : Γ₀) ↦ x1 > x2) ↔
    Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2
have refine_4 : ∀ (h : Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2) (a : Γ₀),
  Membership.mem (γ := Set Γ₀)
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      a →
    ∀ (b : Γ₀),
      Membership.mem (γ := Set Γ₀)
          (Set.range.{u_2, u_3 + 1} (ι := O)
            (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
          b →
        a > b →
          ((fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2) on fun (x : Γ₀) ↦
              if hx : Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x then
                Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x) x hx
              else 1)
            a b
Tactic: classical
  refine ⟨fun h ↦ (h.mapsTo Subtype.val ?_).mono' (by simp), fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩
  · rintro ⟨_, x, rfl⟩
    simp only [← Subtype.coe_le_coe, OneMemClass.coe_one, Set.mem_setOf_eq, Set.mem_range,
      Function.comp_apply]
    intro hx
    obtain ⟨y, rfl⟩ := hv.exists_of_le_one hx
    exact ⟨y, by simp⟩
  · exact fun x ↦ if hx : x ∈ MonoidHom.mrange v then ⟨x, hx⟩ else 1
  · intro
    simp only [Set.mem_range, Function.comp_apply, MonoidHom.mem_mrange, Set.mem_setOf_eq,
      forall_exists_index]
    rintro x rfl
    simp [← Subtype.coe_le_coe, hv.map_le_one]
  · simp [Function.onFun]