-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) x
a :
  ∀ (y : K) (hy : y ∈ (↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K)),
    Membership.mem (α := L)
      (↑(span B
            (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
              ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
        Set L)
      ((IsLocalization.map L f hf : (a : K) → L) y : L)
a₁ :
  ∀ (y z : K),
    Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) y →
      Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K)))
          z →
        ∀
          (hy :
            Membership.mem (α := L)
              (↑(span B
                    (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
                      ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
                Set L)
              ((IsLocalization.map L f hf : (a : K) → L) y : L))
          (hz :
            Membership.mem (α := L)
              (↑(span B
                    (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
                      ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
                Set L)
              ((IsLocalization.map L f hf : (a : K) → L) z : L)),
          Membership.mem (α := L)
            (↑(span B
                  (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
                    ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
              Set L)
            ((IsLocalization.map L f hf : (a : K) → L) (y + z) : L)
a₂ :
  ∀ (a : A) (y : K),
    Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) y →
      ∀
        (hy :
          Membership.mem (α := L)
            (↑(span B
                  (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
                    ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
              Set L)
            ((IsLocalization.map L f hf : (a : K) → L) y : L)),
        Membership.mem (α := L)
          (↑(span B
                (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
                  ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
            Set L)
          ((IsLocalization.map L f hf : (a : K) → L) (a • y) : L)
⊢ Membership.mem (α := L)
    (↑(span B
          (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
            ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) x : L)

Tactic:
refine span_induction (fun y hy ↦ ?_) (by simp) (fun y z _ _ hy hz ↦ ?_)
      (fun a y _ hy ↦ ?_) hx