-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : (↑T : Set A) ⊆ (↑(↑I⁻¹ : Submodule R A) : Set A)
hT' : (↑T' : Set A) ⊆ (↑(↑I : Submodule R A) : Set A)
one_mem : Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) 1
rw :
  ∀
    (one_mem :
      Membership.mem (γ := Submodule R A) (span R (Set.image2 (fun (x1 x2 : A) ↦ x1 * x2) (↑T : Set A) (↑T' : Set A)))
        1),
    Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
      Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A)
        (⇑(mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype) : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)
rw₁ :
  ∀
    (one_mem :
      Membership.mem (γ := Submodule R A) (span R (↑(Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T') : Set A)) 1),
    Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
      Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A)
        (⇑(mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype) : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)
rw₂ rw₃ rw₄ :
  ∀
    (one_mem :
      ∃ (f : A → R),
        Function.support f ⊆ (↑(Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T') : Set A) ∧
          Eq (α := A) (∑ a ∈ Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T', f a • a) 1),
    Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
      Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A)
        (⇑(mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype) : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)
rw₅ :
  let S : Finset A := Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T';
  ∀ (one_mem : ∃ (f : A → R), Function.support f ⊆ (↑S : Set A) ∧ Eq (α := A) (∑ a ∈ S, f a • a) 1),
    Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
      Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A)
        (⇑(mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype) : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)
rw₆ :
  let S : Finset A := Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T';
  ∀ (r : A → R) (hr : Function.support r ⊆ (↑S : Set A) ∧ Eq (α := A) (∑ a ∈ S, r a • a) 1),
    Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
      Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A)
        (⇑(mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype) : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)
rw₇ :
  let S : Finset A := Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T';
  ∀ (r : A → R) (hr : Function.support r ⊆ (↑S : Set A) ∧ Eq (α := A) (∑ a ∈ S, r a • a) 1) (a : (i : ↥S) → A)
    (ha : ∀ (i : ↥S), a i ∈ T) (b : (i : ↥S) → A) (hb : ∀ (i : ↥S), b i ∈ T') (eq : ∀ (i : ↥S), a i * b i = (↑i : A)),
    Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
      Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A)
        (⇑(mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype) : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)
rw₈ :
  let S : Finset A := Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T';
  ∀ (r : A → R) (hr : Function.support r ⊆ (↑S : Set A) ∧ Eq (α := A) (∑ a ∈ S, r a • a) 1) (a : (i : ↥S) → A)
    (ha : ∀ (i : ↥S), a i ∈ T) (b : (i : ↥S) → A) (hb : ∀ (i : ↥S), b i ∈ T') (eq : ∀ (i : ↥S), a i * b i = (↑i : A)),
    Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
      Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A)
        (⇑(mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype) : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)
rw₉ rw₁₀ :
  let S : Finset A := Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T';
  ∀ (r : A → R) (hr : Function.support r ⊆ (↑S : Set A) ∧ Eq (α := A) (∑ a ∈ S, r a • a) 1) (a : (i : ↥S) → A)
    (ha : ∀ (i : ↥S), a i ∈ T) (b : (i : ↥S) → A) (hb : ∀ (i : ↥S), b i ∈ T') (eq : ∀ (i : ↥S), a i * b i = (↑i : A)),
    let f : ↥(↑I : Submodule R A) →ₗ[R] ↥S → R :=
      LinearMap.pi (φ := fun (a : ↥S) ↦ R) fun (i : ↥S) ↦
        ((↑(LinearEquiv.symm (LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯)) :
              LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) :
            LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) ∘ₗ
          (restrict (LinearMap.mulRight R (r (↑i : A) • a i)) ⋯ :
            ↥(↑I : Submodule R A) →ₗ[R] ↥(range (Algebra.linearMap R A)));
    ∀
      (hf :
        ∀ (x : ↥(↑I : Submodule R A)) (i : ↥S),
          (algebraMap R A : (a : R) → A) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x i : R) =
            (↑x : A) * r (↑i : A) • a i),
      Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
        Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A)
          (⇑(mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype) : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)
rw₁₁ :
  let S : Finset A := Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T';
  ∀ (r : A → R) (hr : Function.support r ⊆ (↑S : Set A) ∧ Eq (α := A) (∑ a ∈ S, r a • a) 1) (a : (i : ↥S) → A)
    (ha : ∀ (i : ↥S), a i ∈ T) (b : (i : ↥S) → A) (hb : ∀ (i : ↥S), b i ∈ T') (eq : ∀ (i : ↥S), a i * b i = (↑i : A)),
    let f : ↥(↑I : Submodule R A) →ₗ[R] ↥S → R :=
      LinearMap.pi (φ := fun (a : ↥S) ↦ R) fun (i : ↥S) ↦
        ((↑(LinearEquiv.symm (LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯)) :
              LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) :
            LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) ∘ₗ
          (restrict (LinearMap.mulRight R (r (↑i : A) • a i)) ⋯ :
            ↥(↑I : Submodule R A) →ₗ[R] ↥(range (Algebra.linearMap R A)));
    ∀
      (hf :
        ∀ (x : ↥(↑I : Submodule R A)) (i : ↥S),
          (algebraMap R A : (a : R) → A) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x i : R) =
            (↑x : A) * r (↑i : A) • a i),
      let g : (↥S → R) →ₗ[R] ↥(↑I : Submodule R A) :=
        (lsum R (fun (a : ↥S) ↦ R) ℕ :
            (a : (i : ↥S) → R →ₗ[R] ↥(↑I : Submodule R A)) → ((i : ↥S) → R) →ₗ[R] ↥(↑I : Submodule R A))
          fun (i : ↥S) ↦
          toSpanSingleton R (↥(↑I : Submodule R A)) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b i) ⋯);
      ∀ (hgf : g ∘ₗ f = LinearMap.id),
        Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
          Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A)
            (⇑(mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype) : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)
rw₁₂ :
  let S : Finset A := Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T';
  ∀ (r : A → R) (hr : Function.support r ⊆ (↑S : Set A) ∧ Eq (α := A) (∑ a ∈ S, r a • a) 1) (a : (i : ↥S) → A)
    (ha : ∀ (i : ↥S), a i ∈ T) (b : (i : ↥S) → A) (hb : ∀ (i : ↥S), b i ∈ T') (eq : ∀ (i : ↥S), a i * b i = (↑i : A)),
    let f : ↥(↑I : Submodule R A) →ₗ[R] ↥S → R :=
      LinearMap.pi (φ := fun (a : ↥S) ↦ R) fun (i : ↥S) ↦
        ((↑(LinearEquiv.symm (LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯)) :
              LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) :
            LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) ∘ₗ
          (restrict (LinearMap.mulRight R (r (↑i : A) • a i)) ⋯ :
            ↥(↑I : Submodule R A) →ₗ[R] ↥(range (Algebra.linearMap R A)));
    ∀
      (hf :
        ∀ (x : ↥(↑I : Submodule R A)) (i : ↥S),
          (algebraMap R A : (a : R) → A) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x i : R) =
            (↑x : A) * r (↑i : A) • a i),
      let g : (↥S → R) →ₗ[R] ↥(↑I : Submodule R A) :=
        (lsum R (fun (a : ↥S) ↦ R) ℕ :
            (a : (i : ↥S) → R →ₗ[R] ↥(↑I : Submodule R A)) → ((i : ↥S) → R) →ₗ[R] ↥(↑I : Submodule R A))
          fun (i : ↥S) ↦
          toSpanSingleton R (↥(↑I : Submodule R A)) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b i) ⋯);
      ∀ (hgf : g ∘ₗ f = LinearMap.id),
        let m := mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype;
        Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
          Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A) (⇑m : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)
rw₁₃ :
  let S : Finset A := Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T';
  ∀ (r : A → R) (hr : Function.support r ⊆ (↑S : Set A) ∧ Eq (α := A) (∑ a ∈ S, r a • a) 1) (a : (i : ↥S) → A)
    (ha : ∀ (i : ↥S), a i ∈ T) (b : (i : ↥S) → A) (hb : ∀ (i : ↥S), b i ∈ T') (eq : ∀ (i : ↥S), a i * b i = (↑i : A)),
    let f : ↥(↑I : Submodule R A) →ₗ[R] ↥S → R :=
      LinearMap.pi (φ := fun (a : ↥S) ↦ R) fun (i : ↥S) ↦
        ((↑(LinearEquiv.symm (LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯)) :
              LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) :
            LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) ∘ₗ
          (restrict (LinearMap.mulRight R (r (↑i : A) • a i)) ⋯ :
            ↥(↑I : Submodule R A) →ₗ[R] ↥(range (Algebra.linearMap R A)));
    ∀
      (hf :
        ∀ (x : ↥(↑I : Submodule R A)) (i : ↥S),
          (algebraMap R A : (a : R) → A) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x i : R) =
            (↑x : A) * r (↑i : A) • a i),
      let g : (↥S → R) →ₗ[R] ↥(↑I : Submodule R A) :=
        (lsum R (fun (a : ↥S) ↦ R) ℕ :
            (a : (i : ↥S) → R →ₗ[R] ↥(↑I : Submodule R A)) → ((i : ↥S) → R) →ₗ[R] ↥(↑I : Submodule R A))
          fun (i : ↥S) ↦
          toSpanSingleton R (↥(↑I : Submodule R A)) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b i) ⋯);
      ∀ (hgf : g ∘ₗ f = LinearMap.id),
        let m := mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype;
        ∀
          (eq :
            ((↑(piScalarRight R R A ↥S) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) ∘ₗ
                (lTensor A f : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A ⊗[R] (↥S → R)) =
              (LinearMap.pi (φ := fun (a : ↥S) ↦ A) fun (i : ↥S) ↦ LinearMap.mulRight R (r (↑i : A) • a i)) ∘ₗ m),
          Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
            Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A)
              (⇑m : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)
rw₁₄ :
  let S : Finset A := Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T';
  ∀ (r : A → R) (hr : Function.support r ⊆ (↑S : Set A) ∧ Eq (α := A) (∑ a ∈ S, r a • a) 1) (a : (i : ↥S) → A)
    (ha : ∀ (i : ↥S), a i ∈ T) (b : (i : ↥S) → A) (hb : ∀ (i : ↥S), b i ∈ T') (eq : ∀ (i : ↥S), a i * b i = (↑i : A)),
    let f : ↥(↑I : Submodule R A) →ₗ[R] ↥S → R :=
      LinearMap.pi (φ := fun (a : ↥S) ↦ R) fun (i : ↥S) ↦
        ((↑(LinearEquiv.symm (LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯)) :
              LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) :
            LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) ∘ₗ
          (restrict (LinearMap.mulRight R (r (↑i : A) • a i)) ⋯ :
            ↥(↑I : Submodule R A) →ₗ[R] ↥(range (Algebra.linearMap R A)));
    ∀
      (hf :
        ∀ (x : ↥(↑I : Submodule R A)) (i : ↥S),
          (algebraMap R A : (a : R) → A) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x i : R) =
            (↑x : A) * r (↑i : A) • a i),
      let g : (↥S → R) →ₗ[R] ↥(↑I : Submodule R A) :=
        (lsum R (fun (a : ↥S) ↦ R) ℕ :
            (a : (i : ↥S) → R →ₗ[R] ↥(↑I : Submodule R A)) → ((i : ↥S) → R) →ₗ[R] ↥(↑I : Submodule R A))
          fun (i : ↥S) ↦
          toSpanSingleton R (↥(↑I : Submodule R A)) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b i) ⋯);
      ∀ (hgf : g ∘ₗ f = LinearMap.id),
        let m := mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype;
        ∀
          (eq :
            ((↑(piScalarRight R R A ↥S) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) ∘ₗ
                (lTensor A f : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A ⊗[R] (↥S → R)) =
              (LinearMap.pi (φ := fun (a : ↥S) ↦ A) fun (i : ↥S) ↦ LinearMap.mulRight R (r (↑i : A) • a i)) ∘ₗ m)
          (this :
            Function.Injective.{u_4 + 1, u_4 + 1} (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := ↥S → A)
              (Function.comp (β := A ⊗[R] (↥S → R))
                (⇑(piScalarRight R R A ↥S : A ⊗[R] (↥S → R) ≃ₗ[R] ↥S → A) : (a : A ⊗[R] (↥S → R)) → ↥S → A)
                (⇑(lTensor A f) : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A ⊗[R] (↥S → R)))),
          Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
            Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A)
              (⇑m : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)
rw₁₅ :
  let S : Finset A := Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T';
  ∀ (r : A → R) (hr : Function.support r ⊆ (↑S : Set A) ∧ Eq (α := A) (∑ a ∈ S, r a • a) 1) (a : (i : ↥S) → A)
    (ha : ∀ (i : ↥S), a i ∈ T) (b : (i : ↥S) → A) (hb : ∀ (i : ↥S), b i ∈ T') (eq : ∀ (i : ↥S), a i * b i = (↑i : A)),
    let f : ↥(↑I : Submodule R A) →ₗ[R] ↥S → R :=
      LinearMap.pi (φ := fun (a : ↥S) ↦ R) fun (i : ↥S) ↦
        ((↑(LinearEquiv.symm (LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯)) :
              LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) :
            LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) ∘ₗ
          (restrict (LinearMap.mulRight R (r (↑i : A) • a i)) ⋯ :
            ↥(↑I : Submodule R A) →ₗ[R] ↥(range (Algebra.linearMap R A)));
    ∀
      (hf :
        ∀ (x : ↥(↑I : Submodule R A)) (i : ↥S),
          (algebraMap R A : (a : R) → A) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x i : R) =
            (↑x : A) * r (↑i : A) • a i),
      let g : (↥S → R) →ₗ[R] ↥(↑I : Submodule R A) :=
        (lsum R (fun (a : ↥S) ↦ R) ℕ :
            (a : (i : ↥S) → R →ₗ[R] ↥(↑I : Submodule R A)) → ((i : ↥S) → R) →ₗ[R] ↥(↑I : Submodule R A))
          fun (i : ↥S) ↦
          toSpanSingleton R (↥(↑I : Submodule R A)) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b i) ⋯);
      ∀ (hgf : g ∘ₗ f = LinearMap.id),
        let m := mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype;
        ∀
          (eq :
            ((↑(piScalarRight R R A ↥S) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) ∘ₗ
                (lTensor A f : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A ⊗[R] (↥S → R)) =
              (LinearMap.pi (φ := fun (a : ↥S) ↦ A) fun (i : ↥S) ↦ LinearMap.mulRight R (r (↑i : A) • a i)) ∘ₗ m)
          (this :
            Function.Injective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := ↥S → A)
              (Function.comp (β := A)
                (⇑(LinearMap.pi (φ := fun (a : ↥S) ↦ A) fun (i : ↥S) ↦ LinearMap.mulRight R (r (↑i : A) • a i)) :
                  (a : A) → (i : ↥S) → A)
                (⇑m : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A))),
          Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
            Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A)
              (⇑m : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)
rw₁₆ :
  let S : Finset A := Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T';
  ∀ (r : A → R) (hr : Function.support r ⊆ (↑S : Set A) ∧ Eq (α := A) (∑ a ∈ S, r a • a) 1) (a : (i : ↥S) → A)
    (ha : ∀ (i : ↥S), a i ∈ T) (b : (i : ↥S) → A) (hb : ∀ (i : ↥S), b i ∈ T') (eq : ∀ (i : ↥S), a i * b i = (↑i : A)),
    let f : ↥(↑I : Submodule R A) →ₗ[R] ↥S → R :=
      LinearMap.pi (φ := fun (a : ↥S) ↦ R) fun (i : ↥S) ↦
        ((↑(LinearEquiv.symm (LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯)) :
              LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) :
            LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) ∘ₗ
          (restrict (LinearMap.mulRight R (r (↑i : A) • a i)) ⋯ :
            ↥(↑I : Submodule R A) →ₗ[R] ↥(range (Algebra.linearMap R A)));
    ∀
      (hf :
        ∀ (x : ↥(↑I : Submodule R A)) (i : ↥S),
          (algebraMap R A : (a : R) → A) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x i : R) =
            (↑x : A) * r (↑i : A) • a i),
      let g : (↥S → R) →ₗ[R] ↥(↑I : Submodule R A) :=
        (lsum R (fun (a : ↥S) ↦ R) ℕ :
            (a : (i : ↥S) → R →ₗ[R] ↥(↑I : Submodule R A)) → ((i : ↥S) → R) →ₗ[R] ↥(↑I : Submodule R A))
          fun (i : ↥S) ↦
          toSpanSingleton R (↥(↑I : Submodule R A)) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b i) ⋯);
      ∀ (hgf : g ∘ₗ f = LinearMap.id),
        let m := mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype;
        ∀
          (eq :
            ((↑(piScalarRight R R A ↥S) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) : A ⊗[R] (↥S → R) →ₗ[R] ↥S → A) ∘ₗ
                (lTensor A f : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A ⊗[R] (↥S → R)) =
              (LinearMap.pi (φ := fun (a : ↥S) ↦ A) fun (i : ↥S) ↦ LinearMap.mulRight R (r (↑i : A) • a i)) ∘ₗ m)
          (this :
            Function.Injective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := ↥S → A)
              (Function.comp (β := A)
                (⇑(LinearMap.pi (φ := fun (a : ↥S) ↦ A) fun (i : ↥S) ↦ LinearMap.mulRight R (r (↑i : A) • a i)) :
                  (a : A) → (i : ↥S) → A)
                (⇑m : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A))),
          m.range = ⊤
⊢ Projective.{u, u_4} R ↥(↑I : Submodule R A) ∧
    Function.Bijective (α := A ⊗[R] ↥(↑I : Submodule R A)) (β := A)
      (⇑(mul' R A ∘ₗ lTensor A (↑I : Submodule R A).subtype) : (a : A ⊗[R] ↥(↑I : Submodule R A)) → A)

Tactic:
classical
  rw [← Set.image2_mul, ← Finset.coe_image₂, mem_span_finset] at one_mem
  set S := T.image₂ (· * ·) T'
  obtain ⟨r, hr⟩ := one_mem
  choose a ha b hb eq using fun i : S ↦ Finset.mem_image₂.mp i.2
  let f : I →ₗ[R] S → R := .pi fun i ↦ (LinearEquiv.ofInjective
      (Algebra.linearMap R A) (FaithfulSMul.algebraMap_injective R A)).symm.comp <|
    restrict (mulRight R (r i • a i)) fun x hx ↦ by
      rw [← one_eq_range, ← I.mul_inv]; exact mul_mem_mul hx (I⁻¹.1.smul_mem _ <| hT <| ha i)
  have hf (x : I.1) (i : S) : algebraMap R A (f x i) = x * r i • a i := by
    dsimp [f, ← Algebra.linearMap_apply]
    exact LinearEquiv.ofInjective_symm_apply ..
  let g : (S → R) →ₗ[R] I := .lsum _ _ ℕ fun i ↦ .toSpanSingleton _ _ ⟨b i, hT' <| hb i⟩
  have hgf : g ∘ₗ f = .id := LinearMap.ext fun x ↦ Subtype.ext <| by
    simp only [g, lsum_apply, comp_apply, sum_apply, toSpanSingleton_apply, proj_apply]
    simp_rw [coe_sum, coe_smul, Algebra.smul_def, hf, mul_assoc, ← Finset.mul_sum,
      Algebra.smul_mul_assoc, eq, (Finset.sum_coe_sort ..).trans hr.2, mul_one, id_apply]
  set m := mul' R A ∘ₗ I.1.subtype.lTensor A
  have eq : (piScalarRight R R A S).toLinearMap ∘ₗ f.lTensor A =
      (.pi fun i : S ↦ mulRight R (r i • a i)) ∘ₗ m := by
    ext; simp [(Algebra.smul_def ..).trans (Algebra.commutes ..), hf, m, mul_assoc]
  have := (piScalarRight R R A S).injective.comp <| injective_of_comp_eq_id
    (f.lTensor A) (g.lTensor A) <| by rw [← lTensor_comp, hgf, lTensor_id]
  rw [← LinearEquiv.coe_toLinearMap, ← coe_comp, eq, coe_comp] at this
  refine ⟨.of_split f g hgf, .of_comp this, range_eq_top.mp ?_⟩
  rw [show m = mulMap ⊤ I ∘ₗ (topEquiv.symm.rTensor I.1).toLinearMap by ext; rfl, range_comp,
    LinearEquiv.range, map_top, mulMap_range, top_mul_eq_top_of_mul_eq_one I.inv_mul]

Premises used: Units.val, Submodule.top_mul_eq_top_of_mul_eq_one, HMul.hMul, Submodule.mem_span_finset, Submodule.map_top, Units.inv_mul, LinearMap.range_comp, LinearMap.lTensor, Set.image2_mul, LinearMap.coe_comp, Submodule.subtype, LinearEquiv.coe_toLinearMap, LinearMap.mul', Submodule.mulMap_range, Finset.coe_image₂, LinearEquiv.range, Finset.image₂