R : Type ?u.66348
inst✝¹⁰ : CommRing R
M : Submonoid R
S : Type ?u.66540
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.66777
inst✝⁷ : CommRing P
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
K : Type u_1
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : x ≠ 0
⊢ x *
      (mk' K ↑(sec (nonZeroDivisors A) x).snd
          { val := (sec (nonZeroDivisors A) x).fst,
            property := (_ : (sec (nonZeroDivisors A) x).fst ∈ nonZeroDivisors A) } *
        ↑(algebraMap A K)
          ↑{ val := (sec (nonZeroDivisors A) x).fst,
              property := (_ : (sec (nonZeroDivisors A) x).fst ∈ nonZeroDivisors A) }) =
    ↑(algebraMap A K)
      ↑{ val := (sec (nonZeroDivisors A) x).fst, property := (_ : (sec (nonZeroDivisors A) x).fst ∈ nonZeroDivisors A) }
R : Type ?u.66348
inst✝¹⁰ : CommRing R
M : Submonoid R
S : Type ?u.66540
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.66777
inst✝⁷ : CommRing P
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
K : Type u_1
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : x ≠ 0
⊢ x * IsFractionRing.inv A x = 1
rw [IsFractionRing.inv, dif_neg hx, ←
  IsUnit.mul_left_inj
    (map_units K
      ⟨(sec _ x).1,
        mem_nonZeroDivisors_iff_ne_zero.2 fun h0 =>
          hx <| eq_zero_of_fst_eq_zero (sec_spec (nonZeroDivisors A) x) h0⟩),
  one_mul, mul_assoc]
R : Type ?u.66348
inst✝¹⁰ : CommRing R
M : Submonoid R
S : Type ?u.66540
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.66777
inst✝⁷ : CommRing P
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
K : Type u_1
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : x ≠ 0
⊢ x =
    mk'
      ((fun x => K)
        ↑{ val := (sec (nonZeroDivisors A) x).fst,
            property := (_ : (sec (nonZeroDivisors A) x).fst ∈ nonZeroDivisors A) })
      (↑{ val := (sec (nonZeroDivisors A) x).fst,
          property := (_ : (sec (nonZeroDivisors A) x).fst ∈ nonZeroDivisors A) })
      (sec (nonZeroDivisors A) x).snd
R : Type ?u.66348
inst✝¹⁰ : CommRing R
M : Submonoid R
S : Type ?u.66540
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.66777
inst✝⁷ : CommRing P
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
K : Type u_1
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : x ≠ 0
⊢ x *
      (mk' K ↑(sec (nonZeroDivisors A) x).snd
          { val := (sec (nonZeroDivisors A) x).fst,
            property := (_ : (sec (nonZeroDivisors A) x).fst ∈ nonZeroDivisors A) } *
        ↑(algebraMap A K)
          ↑{ val := (sec (nonZeroDivisors A) x).fst,
              property := (_ : (sec (nonZeroDivisors A) x).fst ∈ nonZeroDivisors A) }) =
    ↑(algebraMap A K)
      ↑{ val := (sec (nonZeroDivisors A) x).fst, property := (_ : (sec (nonZeroDivisors A) x).fst ∈ nonZeroDivisors A) }
rw [mk'_spec, ← eq_mk'_iff_mul_eq]
no goals
R : Type ?u.66348
inst✝¹⁰ : CommRing R
M : Submonoid R
S : Type ?u.66540
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.66777
inst✝⁷ : CommRing P
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
K : Type u_1
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : x ≠ 0
⊢ x =
    mk'
      ((fun x => K)
        ↑{ val := (sec (nonZeroDivisors A) x).fst,
            property := (_ : (sec (nonZeroDivisors A) x).fst ∈ nonZeroDivisors A) })
      (↑{ val := (sec (nonZeroDivisors A) x).fst,
          property := (_ : (sec (nonZeroDivisors A) x).fst ∈ nonZeroDivisors A) })
      (sec (nonZeroDivisors A) x).snd
exact (mk'_sec _ x).symm