awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (hypothesis)
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)
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_1 : ∀ (i : ↥S), a i * b i = (↑i : A)
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
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
m : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A := 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)
have 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))
Tactic: rw [← LinearEquiv.coe_toLinearMap, ← coe_comp, eq, coe_comp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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)
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_1 : ∀ (i : ↥S), a i * b i = (↑i : A)
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
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
m : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A := 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)
have refine : m.range = ⊤
Tactic: refine ⟨.of_split f g hgf, .of_comp this, range_eq_top.mp ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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)
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_1 : ∀ (i : ↥S), a i * b i = (↑i : A)
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
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
m : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A := 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 = ⊤
have rw : (mulMap ⊤ (↑I : Submodule R A) ∘ₗ
      (↑(LinearEquiv.rTensor (↥(↑I : Submodule R A)) (LinearEquiv.symm topEquiv)) :
        A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] ↥⊤ ⊗[R] ↥(↑I : Submodule R A))).range =
  ⊤
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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)
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_1 : ∀ (i : ↥S), a i * b i = (↑i : A)
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
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
m : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A := 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))
rw :
  (mulMap ⊤ (↑I : Submodule R A) ∘ₗ
        (↑(LinearEquiv.rTensor (↥(↑I : Submodule R A)) (LinearEquiv.symm topEquiv)) :
          A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] ↥⊤ ⊗[R] ↥(↑I : Submodule R A))).range =
    ⊤
⊢ m.range = ⊤
have rw₁ : map (mulMap ⊤ (↑I : Submodule R A))
    (range
      (↑(LinearEquiv.rTensor (↥(↑I : Submodule R A)) (LinearEquiv.symm topEquiv)) :
        A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] ↥⊤ ⊗[R] ↥(↑I : Submodule R A))) =
  ⊤
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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)
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_1 : ∀ (i : ↥S), a i * b i = (↑i : A)
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
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
m : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A := 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))
rw :
  (mulMap ⊤ (↑I : Submodule R A) ∘ₗ
        (↑(LinearEquiv.rTensor (↥(↑I : Submodule R A)) (LinearEquiv.symm topEquiv)) :
          A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] ↥⊤ ⊗[R] ↥(↑I : Submodule R A))).range =
    ⊤
rw₁ :
  map (mulMap ⊤ (↑I : Submodule R A))
      (range
        (↑(LinearEquiv.rTensor (↥(↑I : Submodule R A)) (LinearEquiv.symm topEquiv)) :
          A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] ↥⊤ ⊗[R] ↥(↑I : Submodule R A))) =
    ⊤
⊢ m.range = ⊤
have rw₂ : map (M := ↥⊤ ⊗[R] ↥(↑I : Submodule R A)) (mulMap ⊤ (↑I : Submodule R A)) ⊤ = ⊤
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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)
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_1 : ∀ (i : ↥S), a i * b i = (↑i : A)
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
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
m : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A := 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))
rw :
  (mulMap ⊤ (↑I : Submodule R A) ∘ₗ
        (↑(LinearEquiv.rTensor (↥(↑I : Submodule R A)) (LinearEquiv.symm topEquiv)) :
          A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] ↥⊤ ⊗[R] ↥(↑I : Submodule R A))).range =
    ⊤
rw₁ :
  map (mulMap ⊤ (↑I : Submodule R A))
      (range
        (↑(LinearEquiv.rTensor (↥(↑I : Submodule R A)) (LinearEquiv.symm topEquiv)) :
          A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] ↥⊤ ⊗[R] ↥(↑I : Submodule R A))) =
    ⊤
rw₂ : map (M := ↥⊤ ⊗[R] ↥(↑I : Submodule R A)) (mulMap ⊤ (↑I : Submodule R A)) ⊤ = ⊤
⊢ m.range = ⊤
have rw₃ : range (M := ↥⊤ ⊗[R] ↥(↑I : Submodule R A)) (mulMap ⊤ (↑I : Submodule R A)) = ⊤
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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)
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_1 : ∀ (i : ↥S), a i * b i = (↑i : A)
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
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
m : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A := 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))
rw :
  (mulMap ⊤ (↑I : Submodule R A) ∘ₗ
        (↑(LinearEquiv.rTensor (↥(↑I : Submodule R A)) (LinearEquiv.symm topEquiv)) :
          A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] ↥⊤ ⊗[R] ↥(↑I : Submodule R A))).range =
    ⊤
rw₁ :
  map (mulMap ⊤ (↑I : Submodule R A))
      (range
        (↑(LinearEquiv.rTensor (↥(↑I : Submodule R A)) (LinearEquiv.symm topEquiv)) :
          A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] ↥⊤ ⊗[R] ↥(↑I : Submodule R A))) =
    ⊤
rw₂ : map (M := ↥⊤ ⊗[R] ↥(↑I : Submodule R A)) (mulMap ⊤ (↑I : Submodule R A)) ⊤ = ⊤
rw₃ : range (M := ↥⊤ ⊗[R] ↥(↑I : Submodule R A)) (mulMap ⊤ (↑I : Submodule R A)) = ⊤
⊢ m.range = ⊤
have rw₄ : ⊤ * (↑I : Submodule R A) = ⊤
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
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)
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_1 : ∀ (i : ↥S), a i * b i = (↑i : A)
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
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
m : A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] A := 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))
rw :
  (mulMap ⊤ (↑I : Submodule R A) ∘ₗ
        (↑(LinearEquiv.rTensor (↥(↑I : Submodule R A)) (LinearEquiv.symm topEquiv)) :
          A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] ↥⊤ ⊗[R] ↥(↑I : Submodule R A))).range =
    ⊤
rw₁ :
  map (mulMap ⊤ (↑I : Submodule R A))
      (range
        (↑(LinearEquiv.rTensor (↥(↑I : Submodule R A)) (LinearEquiv.symm topEquiv)) :
          A ⊗[R] ↥(↑I : Submodule R A) →ₗ[R] ↥⊤ ⊗[R] ↥(↑I : Submodule R A))) =
    ⊤
rw₂ : map (M := ↥⊤ ⊗[R] ↥(↑I : Submodule R A)) (mulMap ⊤ (↑I : Submodule R A)) ⊤ = ⊤
rw₃ : range (M := ↥⊤ ⊗[R] ↥(↑I : Submodule R A)) (mulMap ⊤ (↑I : Submodule R A)) = ⊤
rw₄ : ⊤ * (↑I : Submodule R A) = ⊤
⊢ m.range = ⊤
have rw₅ : Eq.{u_4 + 1} (α := Submodule R A) ⊤ ⊤
Tactic: 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]