-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst_1 : Field K
A_1 : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A_1
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty.{u_3 + 1} (↑s : Type u_3)
hdir :
  Directed.{u_3, u_3 + 1} (α := Subring K) (ι := { a : LocalSubring K // a ∈ s }) LE.le
    (toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K))
A : LocalSubring K
hA : A ∈ s
a : K
haA : a ∈ A.toSubring
h :
  IsUnit (M := ↥(toSubring { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ }))
    (((Subring.inclusion ⋯ :
            ↥A.toSubring →+*
              ↥(toSubring
                  { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ })) :
          (a : ↥A.toSubring) →
            ↥{ toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ }.toSubring)
        (Subtype.mk (p := fun (x : K) ↦ x ∈ A.toSubring) a haA) :
      ↥(toSubring { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ }))
b : K
hb :
  Membership.mem (γ := Subring K)
    (toSubring { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ }) b
e :
  HMul.hMul (α :=
      ↥(toSubring
          { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ : LocalSubring K }))
      (((Subring.inclusion ⋯ :
              ↥A.toSubring →+*
                ↥(toSubring
                    { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ :
                      LocalSubring K })) :
            (a : ↥A.toSubring) →
              ↥{ toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ }.toSubring)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ A.toSubring) a haA) :
        ↥(toSubring
            { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ :
              LocalSubring K }))
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K)
          (toSubring
            { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ :
              LocalSubring K })
          x)
        b hb) =
    1
B : { a : LocalSubring K // a ∈ s }
hbB : b ∈ (↑B : LocalSubring K).toSubring
C : { a : LocalSubring K // a ∈ s }
hCA :
  LE.le.{u_3} (α := LocalSubring K)
    ((fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K))
      (Subtype.mk (p := fun (a : LocalSubring K) ↦ a ∈ s) A hA))
    ((fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) C)
hCB :
  LE.le.{u_3} (α := LocalSubring K) ((fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) B)
    ((fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) C)
⊢ IsUnit (M := ↥(toSubring ((fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) C)))
    ((Subring.inclusion ⋯ :
          (a : ↥((fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) ⟨A, hA⟩).toSubring) →
            ↥((fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) C).toSubring)
        (Subtype.mk (p := fun (x : K) ↦ x ∈ A.toSubring) a haA) :
      ↥(toSubring ((fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) C)))

Tactic:
isUnit_iff_exists_inv.mpr ⟨⟨b, hCB.1 hbB⟩, Subtype.ext congr(($e).1)⟩

Premises used: Iff.mpr, congrArg, isUnit_iff_exists_inv, id, Subtype.mk, Exists.intro, Subtype.val, Subtype.ext