awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)ˣ
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)
⊢ (↑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
-- 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)ˣ
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)
⊢ (↑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
-- 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)ˣ
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

Tactic:
⟨(isUnit_iff_exists_and_exists.mpr ⟨?_, ?_⟩).unit, Units.ext h.symm⟩

Premises used: Iff.mpr, Set.Mem, setOf, Units.ext, And.intro, Exists.intro, IsUnit.unit, isUnit_iff_exists_and_exists, Set.range, Eq.symm
-- 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)ˣ
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
h₂ : ∃ (c : A), c * (((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1).1 = 1
⊢ Membership.mem (γ := Subgroup (Submodule R A)ˣ)
    (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I

Tactic:
refine ⟨(isUnit_iff_exists_and_exists.mpr ⟨?_, ?_⟩).unit, Units.ext h.symm⟩
-- 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)ˣ
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)
⊢ 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:
simpa [span_mul_span] using congr($h * $h').symm

Premises used: HMul.hMul, congrArg, Submodule.span_mul_span, id, congr, Eq.symm
-- 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)ˣ
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)
⊢ 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
-- 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)ˣ
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
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
⊢ ∃ (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
-- 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)ˣ
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
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)
⊢ (((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1).1 *
      HMul.hMul (α := A) (β := A) ((↑((e' : (a : R) → ↥(↑I⁻¹ : Submodule R A)) 1) : A) : A)
        ((algebraMap R A : (a : R) → A) r.inv : A) =
    1

Tactic:
simp [← mul_assoc, hr, ← map_mul]

Premises used: mul_assoc, map_mul
-- 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)ˣ
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
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:
exact ⟨e' 1 * algebraMap R A r.inv, by simp [← mul_assoc, hr, ← map_mul]⟩
-- 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)ˣ
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)
⊢ 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:
simpa [span_mul_span] using congr($h' * $h).symm

Premises used: HMul.hMul, congrArg, Submodule.span_mul_span, id, congr, Eq.symm
-- 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)ˣ
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)
⊢ 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
-- 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)ˣ
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
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
⊢ ∃ (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
-- 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)ˣ
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
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)
⊢ HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r.inv : A)
        ((↑((e' : (a : R) → ↥(↑I⁻¹ : Submodule R A)) 1) : A) : A) *
      (((↑e : R →ₗ[R] ↥(↑I : Submodule R A)) : (a : R) → ↥(↑I : Submodule R A)) 1).1 =
    1

Tactic:
simp [mul_assoc, hr, ← map_mul]

Premises used: mul_assoc, map_mul
-- 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)ˣ
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
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:
exact ⟨algebraMap R A r.inv * e' 1, by simp [mul_assoc, hr, ← map_mul]⟩
-- 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)ˣ
h :
  Membership.mem (γ := Subgroup (Submodule R A)ˣ)
    (MonoidHom.range (Units.map (↑(spanSingleton R) : A →* Submodule R A))) I
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)ˣ)
⊢ Membership.mem (γ := Subgroup (Submodule R A)ˣ) (MonoidHom.ker (unitsToPic R A)) I

Tactic:
obtain ⟨x, rfl⟩ := h

Premises used: rfl
-- 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
x : Aˣ
x_1 x_2 : R
eq :
  Eq.{u_4 + 1} (α := A) ((LinearMap.toSpanSingleton R A (↑x : A) : (a : R) → A) x_1 : A)
    ((LinearMap.toSpanSingleton R A (↑x : A) : (a : R) → A) x_2 : A)
⊢ Eq.{u_4 + 1} (α := A) ((fun (r : R) ↦ HSMul.hSMul (β := A) r 1) x_1) ((fun (r : R) ↦ HSMul.hSMul (β := A) r 1) x_2)

Tactic:
simpa using congr($eq * x.inv)

Premises used: Units.inv
-- 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
x : Aˣ
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
⊢ 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)

Tactic:
ext
-- 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
x : Aˣ
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:
simp [mem_span_singleton]

Premises used: Submodule.mem_span_singleton
-- 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
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:
exact mk_eq_one_iff.mpr ⟨.symm <| (.ofInjective (LinearMap.toSpanSingleton R A x) fun _ _ eq ↦
      (faithfulSMul_iff_injective_smul_one R A).mp ‹_› <| by simpa using congr($eq * x.inv)) ≪≫ₗ
      .ofEq _ _ (by ext; simp [mem_span_singleton])⟩

Premises used: Iff.mpr, Units.val, LinearEquiv.symm, CommRing.Pic.mk_eq_one_iff, LinearEquiv.ofEq, Nonempty.intro, LinearEquiv.ofInjective, Iff.mp, faithfulSMul_iff_injective_smul_one, LinearEquiv.trans, LinearMap.toSpanSingleton
-- 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
⊢ Function.MulExact.{u_4, u_4, u} (M := Aˣ) (N := (Submodule R A)ˣ) (P := Pic R)
    (⇑(Units.map (↑(spanSingleton R) : A →* Submodule R A)) : (a : Aˣ) → (Submodule R A)ˣ)
    (⇑(unitsToPic R A) : (a : (Submodule R A)ˣ) → Pic R)

Tactic:
MonoidHom.mulExact_iff.mpr (ker_unitsToPic R A)

Premises used: Iff.mpr, Submodule.ker_unitsToPic, MonoidHom.mulExact_iff
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u
M : Type v
A : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst_5 : Flat R M
inst_6 : FaithfulSMul R A
⊢ Function.Injective.{v + 1, u_4 + 1} (α := M) (β := A) (⇑(toAlgebra e) : (a : M) → A)

Tactic:
simpa [toAlgebra] using
    Flat.rTensor_preserves_injective_linearMap _ (FaithfulSMul.algebraMap_injective R A)

Premises used: Module.Flat.toAlgebra, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.PicardGroup
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
⊢ Flat.{u, u_4} R ↥(submoduleAlgebra e)

Tactic:
.of_linearEquiv (submoduleAlgebraEquiv e)

Premises used: Module.Flat.submoduleAlgebraEquiv, Module.Flat.of_linearEquiv
-- Module: Mathlib.RingTheory.PicardGroup
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
inst_13 : Module.Invertible R M
⊢ Module.Invertible.{u, u_4} R ↥(submoduleAlgebra e)

Tactic:
.congr (submoduleAlgebraEquiv e).symm

Premises used: LinearEquiv.symm, Module.Flat.submoduleAlgebraEquiv, Module.Invertible.congr
-- Module: Mathlib.RingTheory.PicardGroup
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)
    (⇑(AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e :
          A ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[A] A) :
      (a : A ⊗[R] ↥(submoduleAlgebra e)) → A)

Tactic:
(AlgebraTensorModule.congr (.refl ..) (submoduleAlgebraEquiv e) ≪≫ₗ e).bijective

Premises used: LinearEquiv.bijective, Module.Flat.submoduleAlgebraEquiv, TensorProduct.AlgebraTensorModule.congr, LinearEquiv.refl, LinearEquiv.trans
-- Module: Mathlib.RingTheory.PicardGroup
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
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)
⊢ 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)

Tactic:
convert! (AlgebraTensorModule.congr (.refl ..) (submoduleAlgebraEquiv e) ≪≫ₗ e).bijective

Premises used: LinearEquiv.bijective, Module.Flat.submoduleAlgebraEquiv, TensorProduct.AlgebraTensorModule.congr, LinearEquiv.refl, LinearEquiv.trans