-- Module: Mathlib.RingTheory.Valuation.Archimedean
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}
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
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}
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
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}
refine_4₂ 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
⊢ (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

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]

Premises used: Set.mem_range, Function.onFun, Valuation.Integers.map_le_one, OneMemClass.coe_one, forall_exists_index, Subtype.coe_le_coe, Set.mem_setOf_eq, Function.comp_apply, rfl, MonoidHom.mem_mrange