awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Invertible R M
f : (P : Ideal R) → [inst_4 : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst_4 : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ map (f P) (f P)
P : Ideal R
h : P.IsMaximal
Rp : Type u_5 := Localization (M := R) P.primeCompl
e : LocalizedModule P.primeCompl M ≃ₗ[Rp] Rp
⊢ Eq (α :=
    LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
      LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
    (↑(TensorProduct.comm R (LocalizedModule P.primeCompl M) (LocalizedModule P.primeCompl M)) :
      LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
        LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
    (((IsLocalizedModule.map P.primeCompl (ff P) (ff P) :
          (M ⊗[R] M →ₗ[R] M ⊗[R] M) →ₗ[R]
            LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
              LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M) :
        (a : M ⊗[R] M →ₗ[R] M ⊗[R] M) →
          LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
            LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
      (↑(LinearEquiv.refl R (M ⊗[R] M)) : M ⊗[R] M →ₗ[R] M ⊗[R] M))
have refine_2 : ∀ (e : LocalizedModule P.primeCompl M ≃ₗ[R] Rp),
  Eq (α :=
    LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
      LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
    (↑(TensorProduct.comm R (LocalizedModule P.primeCompl M) (LocalizedModule P.primeCompl M)) :
      LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
        LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
    (((IsLocalizedModule.map P.primeCompl (ff P) (ff P) :
          (M ⊗[R] M →ₗ[R] M ⊗[R] M) →ₗ[R]
            LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
              LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M) :
        (a : M ⊗[R] M →ₗ[R] M ⊗[R] M) →
          LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M →ₗ[R]
            LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M)
      (↑(LinearEquiv.refl R (M ⊗[R] M)) : M ⊗[R] M →ₗ[R] M ⊗[R] M))
Tactic: have e := e.restrictScalars R
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Invertible R M
f : (P : Ideal R) → [inst_4 : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst_4 : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ map (f P) (f P)
P : Ideal R
h : P.IsMaximal
Rp : Type u_5 := Localization (M := R) P.primeCompl
e_1 : LocalizedModule P.primeCompl M ≃ₗ[Rp] Rp
e : LocalizedModule P.primeCompl M ≃ₗ[R] Rp
x y : LocalizedModule P.primeCompl M
| ((e : (a : LocalizedModule P.primeCompl M) → Rp) y ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) x :
    Rp ⊗[Rp] Rp)
have rw : ((e : (a : LocalizedModule P.primeCompl M) → Rp) x ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) y :
  Rp ⊗[Rp] Rp)
Tactic: rw [← mul_one (e y), ← smul_eq_mul, smul_tmul, smul_eq_mul,
    mul_comm, ← smul_eq_mul, ← smul_tmul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Invertible R M
f : (P : Ideal R) → [inst_4 : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst_4 : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ map (f P) (f P)
P : Ideal R
h : P.IsMaximal
Rp : Type u_5 := Localization (M := R) P.primeCompl
e_1 : LocalizedModule P.primeCompl M ≃ₗ[Rp] Rp
e : LocalizedModule P.primeCompl M ≃ₗ[R] Rp
x y : LocalizedModule P.primeCompl M
⊢ Eq (α := Rp ⊗[Rp] Rp)
    ((e : (a : LocalizedModule P.primeCompl M) → Rp) y ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) x :
      Rp ⊗[Rp] Rp)
    ((e : (a : LocalizedModule P.primeCompl M) → Rp) x ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) y :
      Rp ⊗[Rp] Rp)
have conv_lhs : Eq (α := Rp ⊗[Rp] Rp)
  ((e : (a : LocalizedModule P.primeCompl M) → Rp) y ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) x :
    Rp ⊗[Rp] Rp)
  ((e : (a : LocalizedModule P.primeCompl M) → Rp) x ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) y :
    Rp ⊗[Rp] Rp)
Tactic: conv_lhs => rw [← mul_one (e y), ← smul_eq_mul, smul_tmul, smul_eq_mul,
    mul_comm, ← smul_eq_mul, ← smul_tmul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Invertible R M
f : (P : Ideal R) → [inst_4 : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst_4 : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun (P : Ideal R) [P.IsMaximal] ↦ map (f P) (f P)
P : Ideal R
h : P.IsMaximal
Rp : Type u_5 := Localization (M := R) P.primeCompl
e_1 : LocalizedModule P.primeCompl M ≃ₗ[Rp] Rp
e : LocalizedModule P.primeCompl M ≃ₗ[R] Rp
x y : LocalizedModule P.primeCompl M
conv_lhs :
  Eq (α := Rp ⊗[Rp] Rp)
    ((e : (a : LocalizedModule P.primeCompl M) → Rp) y ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) x :
      Rp ⊗[Rp] Rp)
    ((e : (a : LocalizedModule P.primeCompl M) → Rp) x ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) y :
      Rp ⊗[Rp] Rp)
⊢ Eq (α := Rp ⊗[Rp] Rp)
    ((e : (a : LocalizedModule P.primeCompl M) → Rp) y ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) x :
      Rp ⊗[Rp] Rp)
    ((e : (a : LocalizedModule P.primeCompl M) → Rp) x ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) y :
      Rp ⊗[Rp] Rp)
have refine_2 : Eq (α := Rp ⊗[Rp] Rp)
  ((e : (a : LocalizedModule P.primeCompl M) → Rp) x ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) y :
    Rp ⊗[Rp] Rp)
  ((e : (a : LocalizedModule P.primeCompl M) → Rp) x ⊗ₜ[Rp] (e : (a : LocalizedModule P.primeCompl M) → Rp) y :
    Rp ⊗[Rp] Rp)
Tactic: conv_lhs => rw [← mul_one (e y), ← smul_eq_mul, smul_tmul, smul_eq_mul,
    mul_comm, ← smul_eq_mul, ← smul_tmul, smul_eq_mul, mul_one]
-- 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)ˣ
⊢ 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)
have obtain : ∀ (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),
  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: obtain ⟨T, T', hT, hT', one_mem⟩ := mem_span_mul_finite_of_mem_mul (I.inv_mul ▸ one_le.mp le_rfl)
-- 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)
one_mem : Membership.mem (γ := Submodule R A) (span R ((↑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)
have 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
Tactic: rw [← Set.image2_mul, ← Finset.coe_image₂, mem_span_finset] at one_mem
Cleared hypotheses: one_mem
-- 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'
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)
have obtain : ∀ (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)
Tactic: obtain ⟨r, hr⟩ := one_mem
Cleared hypotheses: one_mem
-- 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
⊢ 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)
have choose : ∀ (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)
Tactic: choose a ha b hb eq using fun i : S ↦ Finset.mem_image₂.mp i.2
-- 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 : ∀ (i : ↥S), a i * b i = (↑i : A)
i : ↥S
x : A
hx : x ∈ (↑I : Submodule R A)
⊢ Membership.mem (α := A) (γ := Submodule R A) (range (Algebra.linearMap R A))
    ((LinearMap.mulRight R (r (↑i : A) • a i) : (a : A) → A) x : A)
have rw : Membership.mem (α := A) ((↑I : Submodule R A) * (↑I⁻¹ : Submodule R A))
  ((LinearMap.mulRight R (r (↑i : A) • a i) : (a : A) → A) x : A)
Tactic: rw [← one_eq_range, ← I.mul_inv]
-- 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 : ∀ (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)))
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
have dsimp : (Algebra.linearMap R A : (a : R) → A)
    ((LinearEquiv.symm (LinearEquiv.ofInjective (Algebra.linearMap R A) sorry) : (a : ↥(Algebra.linearMap R A).range) → R)
        ((restrict (LinearMap.mulRight R (r (↑i : A) • a i)) sorry :
              (a : ↥(↑I : Submodule R A)) → ↥(Algebra.linearMap R A).range)
            x :
          ↥(range (Algebra.linearMap R A))) :
      R) =
  (↑x : A) * r (↑i : A) • a i
Tactic: dsimp [f, ← Algebra.linearMap_apply]
-- 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 : ∀ (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)))
⊢ 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)
have 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
Tactic: 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 ..
-- 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 : ∀ (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) ⋯)
x : ↥(↑I : Submodule R A)
⊢ Eq.{u_4 + 1} (α := A) (↑((g ∘ₗ f : (a : ↥(↑I : Submodule R A)) → ↥(↑I : Submodule R A)) x) : A)
    (↑((LinearMap.id : (a : ↥(↑I : Submodule R A)) → ↥(↑I : Submodule R A)) x) : A)
have simp : Eq.{u_4 + 1} (α := A)
  (↑(∑ x_1 : ↥S,
        HSMul.hSMul.{u, u_4, u_4} (α := R) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x x_1 : R)
          (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b x_1) sorry)) :
    A)
  (↑((LinearMap.id : (a : ↥(↑I : Submodule R A)) → ↥(↑I : Submodule R A)) x) : A)
Tactic: simp only [g, lsum_apply, comp_apply, sum_apply, toSpanSingleton_apply, proj_apply]
-- 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 : ∀ (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) ⋯)
x : ↥(↑I : Submodule R A)
⊢ Eq.{u_4 + 1} (α := A)
    (↑(∑ x_1 : ↥S,
          HSMul.hSMul.{u, u_4, u_4} (α := R) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x x_1 : R)
            (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b x_1) ⋯)) :
      A)
    (↑((LinearMap.id : (a : ↥(↑I : Submodule R A)) → ↥(↑I : Submodule R A)) x) : A)
have simp_rw : Eq.{u_4 + 1} (α := A)
  (∑ i : ↥S,
    (↑(HSMul.hSMul.{u, u_4, u_4} (α := R) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x i : R)
          (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b i) sorry)) :
      A))
  (↑((LinearMap.id : (a : ↥(↑I : Submodule R A)) → ↥(↑I : Submodule R A)) x) : A)
Tactic: 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]
-- 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 : ∀ (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) ⋯)
x : ↥(↑I : Submodule R A)
simp_rw :
  Eq.{u_4 + 1} (α := A)
    (∑ i : ↥S,
      (↑(HSMul.hSMul.{u, u_4, u_4} (α := R) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x i : R)
            (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b i) ⋯)) :
        A))
    (↑((LinearMap.id : (a : ↥(↑I : Submodule R A)) → ↥(↑I : Submodule R A)) x) : A)
⊢ Eq.{u_4 + 1} (α := A)
    (↑(∑ x_1 : ↥S,
          HSMul.hSMul.{u, u_4, u_4} (α := R) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x x_1 : R)
            (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b x_1) ⋯)) :
      A)
    (↑((LinearMap.id : (a : ↥(↑I : Submodule R A)) → ↥(↑I : Submodule R A)) x) : A)
have simp_rw₁ : Eq.{u_4 + 1} (α := A)
  (∑ x_1 : ↥S, HSMul.hSMul.{u, u_4, u_4} (α := R) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x x_1 : R) (b x_1))
  (↑((LinearMap.id : (a : ↥(↑I : Submodule R A)) → ↥(↑I : Submodule R A)) x) : A)
Tactic: 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]