awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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 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)
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]
Cleared hypotheses: one_mem
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Semiring A
inst_10 : Algebra R A
inst_11 : FaithfulSMul R A
I J : (Submodule R A)ˣ
⊢ ↥(↑I : Submodule R A) ⊗[R] ↥(↑J : Submodule R A) ≃ₗ[R] ↥(↑(I * J) : Submodule R A)
have refine : Function.Injective (α := ↥(↑I : Submodule R A) ⊗[R] ↥(↑J : Submodule R A)) (β := A)
  (Function.comp (β := ↥(↑(I * J) : Submodule R A))
    (⇑(↑(I * J) : Submodule R A).subtype : (a : ↥(↑(I * J) : Submodule R A)) → A)
    (⇑((↑I : Submodule R A).mulMap' (↑J : Submodule R A)) :
      (a : ↥(↑I : Submodule R A) ⊗[R] ↥(↑J : Submodule R A)) → ↥(↑(I * J) : Submodule R A)))
Tactic: refine .ofBijective _ ⟨.of_comp (f := Submodule.subtype _) ?_, mulMap'_surjective _ _⟩
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Semiring A
inst_10 : Algebra R A
inst_11 : FaithfulSMul R A
I_1 J_1 I J : (Submodule R A)ˣ
⊢ Pic.mk.{u, u_4} R ↥(↑(I * J) : Submodule R A) =
    HMul.hMul (α := Pic R) (Pic.mk.{u, u_4} R ↥(↑I : Submodule R A)) (Pic.mk.{u, u_4} R ↥(↑J : Submodule R A))
have rw : Nonempty.{u_4 + 1} (↥(↑(I * J) : Submodule R A) ≃ₗ[R] ↥(↑I : Submodule R A) ⊗[R] ↥(↑J : Submodule R A))
Tactic: rw [← mk_tensor, mk_eq_mk_iff]
-- 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
⊢ Eq (α := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A))
    (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A)))
have h : ∀ (I : (Submodule R A)ˣ),
  Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I ↔
    Membership.mem (γ := Subgroup (Submodule R A)ˣ)
      (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I
Tactic: ext I
-- 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)ˣ
⊢ Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I ↔
    Membership.mem (γ := Subgroup (Submodule R A)ˣ)
      (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I
have h : Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I →
  Membership.mem (γ := Subgroup (Submodule R A)ˣ)
    (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I
Tactic: constructor
-- 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)ˣ
h :
  Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I →
    Membership.mem (γ := Subgroup (Submodule R A)ˣ)
      (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I
⊢ Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I ↔
    Membership.mem (γ := Subgroup (Submodule R A)ˣ)
      (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I
have h₁ : Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A)))
    I →
  Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I
Tactic: constructor
-- 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)ˣ
h : Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I
⊢ Membership.mem (γ := Subgroup (Submodule R A)ˣ)
    (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I
have h₁ : ∀ (e : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I : Submodule R A)),
  Membership.mem (γ := Subgroup (Submodule R A)ˣ)
    (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I
Tactic: have e := (mk_eq_one_iff.mp h).some.symm
-- 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)ˣ
h : Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I
e : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I : Submodule R A)
⊢ Membership.mem (γ := Subgroup (Submodule R A)ˣ)
    (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I
have h₁ : ∀ (e' : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I⁻¹ : Submodule R A)),
  Membership.mem (γ := Subgroup (Submodule R A)ˣ)
    (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I
Tactic: have e' := (mk_eq_one_iff.mp (inv_mem h)).some.symm
-- 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)ˣ
h : Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I
e : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I : Submodule R A)
e' : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I⁻¹ : Submodule R A)
⊢ Membership.mem (γ := Subgroup (Submodule R A)ˣ)
    (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I
have h₁ : (↑I : Submodule R A) = R ∙ (↑(((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1) : A)
Tactic: have h := eq_span_singleton_of_surjective e.surjective
-- 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)ˣ
h_1 : Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I
e : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I : Submodule R A)
e' : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I⁻¹ : Submodule R A)
h : (↑I : Submodule R A) = R ∙ (↑(((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1) : A)
⊢ Membership.mem (γ := Subgroup (Submodule R A)ˣ)
    (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I
have h' : (↑I⁻¹ : Submodule R A) = R ∙ (↑(((↑e' : R →ₗ[R] ↥(↑I⁻¹ : Submodule R A)) : (a : R) → ↥(↑I⁻¹ : Submodule R A)) 1) : A)
Tactic: have h' := eq_span_singleton_of_surjective e'.surjective
-- 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)ˣ
h_1 : Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I
e : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I : Submodule R A)
e' : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I⁻¹ : Submodule R A)
h : (↑I : Submodule R A) = R ∙ (↑(((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1) : A)
h' :
  (↑I⁻¹ : Submodule R A) = R ∙ (↑(((↑e' : R →ₗ[R] ↥(↑I⁻¹ : Submodule R A)) : (a : R) → ↥(↑I⁻¹ : Submodule R A)) 1) : A)
⊢ Membership.mem (γ := Subgroup (Submodule R A)ˣ)
    (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I
have h₁ : ∃ (b : A), (((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1).1 * b = 1
Tactic: refine ⟨(isUnit_iff_exists_and_exists.mpr ⟨?_, ?_⟩).unit, Units.ext h.symm⟩
-- 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)ˣ
h_1 : Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I
e : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I : Submodule R A)
e' : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I⁻¹ : Submodule R A)
h : (↑I : Submodule R A) = R ∙ (↑(((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1) : A)
h' :
  (↑I⁻¹ : Submodule R A) = R ∙ (↑(((↑e' : R →ₗ[R] ↥(↑I⁻¹ : Submodule R A)) : (a : R) → ↥(↑I⁻¹ : Submodule R A)) 1) : A)
h₁ : ∃ (b : A), (((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1).1 * b = 1
⊢ Membership.mem (γ := Subgroup (Submodule R A)ˣ)
    (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I
have h₂ : ∃ (c : A), c * (((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1).1 = 1
Tactic: refine ⟨(isUnit_iff_exists_and_exists.mpr ⟨?_, ?_⟩).unit, Units.ext h.symm⟩
-- 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)ˣ
h_1 : Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I
e : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I : Submodule R A)
e' : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I⁻¹ : Submodule R A)
h : (↑I : Submodule R A) = R ∙ (↑(((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1) : A)
h' :
  (↑I⁻¹ : Submodule R A) = R ∙ (↑(((↑e' : R →ₗ[R] ↥(↑I⁻¹ : Submodule R A)) : (a : R) → ↥(↑I⁻¹ : Submodule R A)) 1) : A)
⊢ ∃ (b : A), (((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1).1 * b = 1
have this : Eq (α := Submodule R A)
  (R ∙
    HMul.hMul (α := A) (↑((e : (a : R) → ↥(↑I : Submodule R A)) 1) : A)
      (↑((e' : (a : R) → ↥(↑I⁻¹ : Submodule R A)) 1) : A))
  1
Tactic: have : span R {(e 1).1 * e' 1} = 1 := by simpa [span_mul_span] using congr($h * $h').symm
-- 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)ˣ
h_1 : Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I
e : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I : Submodule R A)
e' : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I⁻¹ : Submodule R A)
h : (↑I : Submodule R A) = R ∙ (↑(((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1) : A)
h' :
  (↑I⁻¹ : Submodule R A) = R ∙ (↑(((↑e' : R →ₗ[R] ↥(↑I⁻¹ : Submodule R A)) : (a : R) → ↥(↑I⁻¹ : Submodule R A)) 1) : A)
this :
  Eq (α := Submodule R A)
    (R ∙
      HMul.hMul (α := A) (↑((e : (a : R) → ↥(↑I : Submodule R A)) 1) : A)
        (↑((e' : (a : R) → ↥(↑I⁻¹ : Submodule R A)) 1) : A))
    1
⊢ ∃ (b : A), (((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1).1 * b = 1
have h₁ : ∀ (r : Rˣ)
  (hr :
    HMul.hMul (α := A) (↑((e : (a : R) → ↥(↑I : Submodule R A)) 1) : A)
        (↑((e' : (a : R) → ↥(↑I⁻¹ : Submodule R A)) 1) : A) =
      (algebraMap R A : (a : R) → A) (↑r : R)),
  ∃ (b : A), (((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1).1 * b = 1
Tactic: have ⟨r, hr⟩ := span_singleton_eq_one_iff.mp this
-- 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)ˣ
h_1 : Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I
e : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I : Submodule R A)
e' : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I⁻¹ : Submodule R A)
h : (↑I : Submodule R A) = R ∙ (↑(((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1) : A)
h' :
  (↑I⁻¹ : Submodule R A) = R ∙ (↑(((↑e' : R →ₗ[R] ↥(↑I⁻¹ : Submodule R A)) : (a : R) → ↥(↑I⁻¹ : Submodule R A)) 1) : A)
⊢ ∃ (c : A), c * (((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1).1 = 1
have this : Eq (α := Submodule R A)
  (R ∙
    HMul.hMul (α := A) (↑((e' : (a : R) → ↥(↑I⁻¹ : Submodule R A)) 1) : A)
      (↑((e : (a : R) → ↥(↑I : Submodule R A)) 1) : A))
  1
Tactic: have : span R {(e' 1).1 * e 1} = 1 := by simpa [span_mul_span] using congr($h' * $h).symm
-- 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)ˣ
h_1 : Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I
e : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I : Submodule R A)
e' : LinearEquiv.{u, u, u, u_4} (RingHom.id R) R ↥(↑I⁻¹ : Submodule R A)
h : (↑I : Submodule R A) = R ∙ (↑(((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1) : A)
h' :
  (↑I⁻¹ : Submodule R A) = R ∙ (↑(((↑e' : R →ₗ[R] ↥(↑I⁻¹ : Submodule R A)) : (a : R) → ↥(↑I⁻¹ : Submodule R A)) 1) : A)
this :
  Eq (α := Submodule R A)
    (R ∙
      HMul.hMul (α := A) (↑((e' : (a : R) → ↥(↑I⁻¹ : Submodule R A)) 1) : A)
        (↑((e : (a : R) → ↥(↑I : Submodule R A)) 1) : A))
    1
⊢ ∃ (c : A), c * (((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1).1 = 1
have h₁ : ∀ (r : Rˣ)
  (hr :
    HMul.hMul (α := A) (↑((e' : (a : R) → ↥(↑I⁻¹ : Submodule R A)) 1) : A)
        (↑((e : (a : R) → ↥(↑I : Submodule R A)) 1) : A) =
      (algebraMap R A : (a : R) → A) (↑r : R)),
  ∃ (c : A), c * (((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1).1 = 1
Tactic: have ⟨r, hr⟩ := span_singleton_eq_one_iff.mp 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)ˣ
h :
  Membership.mem (γ := Subgroup (Submodule R A)ˣ)
    (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I
⊢ Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I
have h₁ : ∀ (x : Aˣ),
  Membership.mem (α := (Submodule R A)ˣ) (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A))
    ((Units.map (↑(spanSingleton R) : A →* Submodule R A) : (a : Aˣ) → (Submodule R A)ˣ) x : (Submodule R A)ˣ)
Tactic: obtain ⟨x, rfl⟩ := h
Cleared hypotheses: I, h
-- 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
x : Aˣ
⊢ Eq (α := Submodule R A) (LinearMap.range (LinearMap.toSpanSingleton R A (↑x : A)))
    (↑((Units.map (↑(spanSingleton R) : A →* Submodule R A) : (a : Aˣ) → (Submodule R A)ˣ) x) : Submodule R A)
have h : ∀ (x_1 : A),
  Membership.mem (γ := Submodule R A) (LinearMap.range (LinearMap.toSpanSingleton R A (↑x : A))) x_1 ↔
    Membership.mem (γ := Submodule R A)
      (↑((Units.map (↑(spanSingleton R) : A →* Submodule R A) : (a : Aˣ) → (Submodule R A)ˣ) x) : Submodule R A) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
⊢ Function.Bijective (α := A ⊗[R] ↥(submoduleAlgebra e)) (β := A)
    (⇑(LinearMap.mul'' R A ∘ₗ
          ((AlgebraTensorModule.lTensor A A :
                (↥(submoduleAlgebra e) →ₗ[R] A) →ₗ[R] A ⊗[R] ↥(submoduleAlgebra e) →ₗ[A] A ⊗[R] A) :
              (a : ↥(submoduleAlgebra e) →ₗ[R] A) → A ⊗[R] ↥(submoduleAlgebra e) →ₗ[A] A ⊗[R] A)
            (submoduleAlgebra e).subtype) :
      (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
have h : Eq (α := A ⊗[R] ↥(submoduleAlgebra e) → A)
  (⇑(LinearMap.mul'' R A ∘ₗ
        ((AlgebraTensorModule.lTensor A A :
              (↥(submoduleAlgebra e) →ₗ[R] A) →ₗ[R] A ⊗[R] ↥(submoduleAlgebra e) →ₗ[A] A ⊗[R] A) :
            (a : ↥(submoduleAlgebra e) →ₗ[R] A) → A ⊗[R] ↥(submoduleAlgebra e) →ₗ[A] A ⊗[R] A)
          (submoduleAlgebra e).subtype) :
    (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
  (⇑(AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e :
        A ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[A] A) :
    (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
Tactic: convert! (AlgebraTensorModule.congr (.refl ..) (submoduleAlgebraEquiv e) ≪≫ₗ e).bijective
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
⊢ Eq (α := A ⊗[R] ↥(submoduleAlgebra e) → A)
    (⇑(LinearMap.mul'' R A ∘ₗ
          ((AlgebraTensorModule.lTensor A A :
                (↥(submoduleAlgebra e) →ₗ[R] A) →ₗ[R] A ⊗[R] ↥(submoduleAlgebra e) →ₗ[A] A ⊗[R] A) :
              (a : ↥(submoduleAlgebra e) →ₗ[R] A) → A ⊗[R] ↥(submoduleAlgebra e) →ₗ[A] A ⊗[R] A)
            (submoduleAlgebra e).subtype) :
      (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
    (⇑(AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e :
          A ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[A] A) :
      (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
have h : ∀ (x : A ⊗[R] ↥(submoduleAlgebra e)),
  Eq (α := A)
    ((LinearMap.mul'' R A ∘ₗ
            ((AlgebraTensorModule.lTensor A A :
                  (↥(submoduleAlgebra e) →ₗ[R] A) →ₗ[R] A ⊗[R] ↥(submoduleAlgebra e) →ₗ[A] A ⊗[R] A) :
                (a : ↥(submoduleAlgebra e) →ₗ[R] A) → A ⊗[R] ↥(submoduleAlgebra e) →ₗ[A] A ⊗[R] A)
              (submoduleAlgebra e).subtype :
          (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
        x :
      A)
    (((AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e :
            A ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[A] A) :
          (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
        x :
      A)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Semiring A
inst_10 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_11 : Flat R M
inst_12 : FaithfulSMul R A
x : A ⊗[R] ↥(submoduleAlgebra e)
⊢ Eq (α := A)
    ((LinearMap.mul'' R A ∘ₗ
            ((AlgebraTensorModule.lTensor A A :
                  (↥(submoduleAlgebra e) →ₗ[R] A) →ₗ[R] A ⊗[R] ↥(submoduleAlgebra e) →ₗ[A] A ⊗[R] A) :
                (a : ↥(submoduleAlgebra e) →ₗ[R] A) → A ⊗[R] ↥(submoduleAlgebra e) →ₗ[A] A ⊗[R] A)
              (submoduleAlgebra e).subtype :
          (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
        x :
      A)
    (((AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e :
            A ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[A] A) :
          (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
        x :
      A)
have h : ∀ (x : A) (y : ↥(submoduleAlgebra e)),
  Eq (α := A)
    ((LinearMap.mul'' R A ∘ₗ
            ((AlgebraTensorModule.lTensor A A :
                  (↥(submoduleAlgebra e) →ₗ[R] A) →ₗ[R] A ⊗[R] ↥(submoduleAlgebra e) →ₗ[A] A ⊗[R] A) :
                (a : ↥(submoduleAlgebra e) →ₗ[R] A) → A ⊗[R] ↥(submoduleAlgebra e) →ₗ[A] A ⊗[R] A)
              (submoduleAlgebra e).subtype :
          (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
        (x ⊗ₜ[R] y) :
      A)
    (((AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e :
            A ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[A] A) :
          (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)
        (x ⊗ₜ[R] y) :
      A)
Tactic: refine x.induction_on (by simp) ?_ (by simp +contextual)