awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis.{u_1, u, v} ι R ↥O
hNO : N ≤ O
ϕ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_3 : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
i : ι
rw :
  ∀ (hϕ : ∀ (ψ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R), ¬⊥ < ψ.submoduleImage N)
    [inst_4 : (ϕ.submoduleImage N).IsPrincipal] (hgen : generator (ϕ.submoduleImage N) = 0) (x : M) (hx : x ∈ N)
    (i : ι),
    Eq.{u + 1} (α := R)
      ((((b.repr : (a : ↥O) → ι →₀ R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x ⋯) : ι →₀ R) : (a : ι) → R) i : R)
      (((b.repr : (a : ↥O) → ι →₀ R) 0 : (a : ι) → R) i : R)
⊢ Eq.{u + 1} (α := R)
    ((((b.repr : (a : ↥O) → ι →₀ R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x ⋯) : ι →₀ R) : (a : ι) → R) i : R)
    (((b.repr : (a : ↥O) → ι →₀ R) 0 : (a : ι) → R) i : R)

Tactic:
rw [(eq_bot_iff_generator_eq_zero _).mpr hgen] at hϕ

Premises used: Iff.mpr, Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis.{u_1, u, v} ι R ↥O
hNO : N ≤ O
ϕ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R), ¬⊥ < ψ.submoduleImage N
inst_3 : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
i : ι
rw :
  Eq.{u + 1} (α := R)
    ((((b.repr : (a : ↥O) → ι →₀ R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x ⋯) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
⊢ Eq.{u + 1} (α := R)
    ((((b.repr : (a : ↥O) → ι →₀ R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x ⋯) : ι →₀ R) : (a : ι) → R) i : R)
    (((b.repr : (a : ↥O) → ι →₀ R) 0 : (a : ι) → R) i : R)

Tactic:
rw [map_zero, Finsupp.zero_apply]

Premises used: map_zero, Finsupp.zero_apply
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis.{u_1, u, v} ι R ↥O
hNO : N ≤ O
ϕ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R), ¬⊥ < ψ.submoduleImage N
inst_3 : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
i : ι
⊢ Eq.{u + 1} (α := R)
    ((((b.repr : (a : ↥O) → ι →₀ R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x ⋯) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)

Tactic:
(Submodule.eq_bot_iff _).mp (not_bot_lt_iff.1 <| hϕ (Finsupp.lapply i ∘ₗ ↑b.repr)) _ ?_

Premises used: Module.Basis.repr, LinearMap.comp, LinearEquiv.toLinearMap, Iff.mp, not_bot_lt_iff, Submodule.eq_bot_iff, Finsupp.lapply
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis.{u_1, u, v} ι R ↥O
hNO : N ≤ O
ϕ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R), ¬⊥ < ψ.submoduleImage N
inst_3 : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
i : ι
refine :
  Membership.mem (α := R) ((Finsupp.lapply i ∘ₗ (↑b.repr : ↥O →ₗ[R] ι →₀ R)).submoduleImage N)
    ((((b.repr : (a : ↥O) → ι →₀ R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x ⋯) : ι →₀ R) : (a : ι) → R) i : R)
⊢ Eq.{u + 1} (α := R)
    ((((b.repr : (a : ↥O) → ι →₀ R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x ⋯) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)

Tactic:
refine (Submodule.eq_bot_iff _).mp (not_bot_lt_iff.1 <| hϕ (Finsupp.lapply i ∘ₗ ↑b.repr)) _ ?_

Premises used: Module.Basis.repr, LinearMap.comp, LinearEquiv.toLinearMap, Iff.mp, not_bot_lt_iff, Submodule.eq_bot_iff, Finsupp.lapply
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis.{u_1, u, v} ι R ↥O
hNO : N ≤ O
ϕ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R), ¬⊥ < ψ.submoduleImage N
inst_3 : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
i : ι
⊢ Membership.mem (α := R) ((Finsupp.lapply i ∘ₗ (↑b.repr : ↥O →ₗ[R] ι →₀ R)).submoduleImage N)
    ((((b.repr : (a : ↥O) → ι →₀ R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x ⋯) : ι →₀ R) : (a : ι) → R) i : R)

Tactic:
(LinearMap.mem_submoduleImage_of_le hNO).mpr ⟨x, hx, rfl⟩

Premises used: Iff.mpr, LinearMap.mem_submoduleImage_of_le, Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis.{u_1, u, v} ι R ↥O
hNO : N ≤ O
ϕ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R), ¬⊥ < ψ.submoduleImage N
inst_3 : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
i : ι
⊢ Membership.mem (α := R) ((Finsupp.lapply i ∘ₗ (↑b.repr : ↥O →ₗ[R] ι →₀ R)).submoduleImage N)
    ((((b.repr : (a : ↥O) → ι →₀ R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x ⋯) : ι →₀ R) : (a : ι) → R) i : R)

Tactic:
exact (LinearMap.mem_submoduleImage_of_le hNO).mpr ⟨x, hx, rfl⟩

Premises used: Iff.mpr, LinearMap.mem_submoduleImage_of_le, Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : Submodule.IsPrincipal I
x : R
hx : x ∈ I
simp_rw : Membership.mem (γ := Ideal R) (Ideal.span {x}) (generator I) ↔ I ≤ Ideal.span {x}
⊢ x ∣ generator I ↔ I = Ideal.span {x}

Tactic:
simp_rw [le_antisymm_iff, I.span_singleton_le_iff_mem.2 hx, and_true, ← Ideal.mem_span_singleton]

Premises used: Iff.mpr, and_true, Ideal.span_singleton_le_iff_mem, le_antisymm_iff, Ideal.mem_span_singleton
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : Submodule.IsPrincipal I
x : R
hx : x ∈ I
rw : Membership.mem (γ := Submodule R R) (Ideal.span {x}) (generator I)
| I ≤ Ideal.span {x}

Tactic:
rw [← span_singleton_generator I, Submodule.span_singleton_le_iff_mem]

Premises used: Submodule.IsPrincipal.span_singleton_generator, Submodule.span_singleton_le_iff_mem
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : Submodule.IsPrincipal I
x : R
hx : x ∈ I
conv_rhs : Membership.mem (γ := Ideal R) (Ideal.span {x}) (generator I) ↔ I ≤ Ideal.span {x}
conv_rhs₁ :
  Membership.mem (γ := Ideal R) (Ideal.span {x}) (generator I) ↔
    Membership.mem (γ := Submodule R R) (Ideal.span {x}) (generator I)
⊢ Membership.mem (γ := Ideal R) (Ideal.span {x}) (generator I) ↔ I ≤ Ideal.span {x}

Tactic:
conv_rhs => rw [← span_singleton_generator I, Submodule.span_singleton_le_iff_mem]

Premises used: Submodule.IsPrincipal.span_singleton_generator, Submodule.span_singleton_le_iff_mem
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
⊢ d ∣ a

Tactic:
have d_dvd_left : d ∣ a := (mem_iff_generator_dvd _).mp (subset_span (mem_insert _ _))
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
⊢ d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)

Tactic:
have d_dvd_right : d ∣ ψ ⟨y, hNO yN⟩ :=
    (mem_iff_generator_dvd _).mp (subset_span (mem_insert_of_mem _ (mem_singleton _)))
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
⊢ generator (ϕ.submoduleImage N) ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)

Tactic:
dvd_trans ?_ d_dvd_right

Premises used: dvd_trans
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
refine : generator (ϕ.submoduleImage N) ∣ d
⊢ generator (ϕ.submoduleImage N) ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)

Tactic:
refine dvd_trans ?_ d_dvd_right

Premises used: dvd_trans
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
rw :
  Eq (α := Ideal R)
    (R ∙
      generator
        (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)))))
    (R ∙ generator (ϕ.submoduleImage N))
rw₁ :
  Membership.mem (γ := Ideal R)
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
    (generator (ϕ.submoduleImage N))
⊢ generator (ϕ.submoduleImage N) ∣ d

Tactic:
rw [dvd_generator_iff, Ideal.span, ←
    span_singleton_generator (Submodule.span R {a, ψ ⟨y, hNO yN⟩})]

Premises used: Insert.insert, dvd_generator_iff, Subtype.mk, Submodule.span, Submodule.IsPrincipal.span_singleton_generator, Ideal.span, Singleton.singleton, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
obtain :
  ∀ (r₁ r₂' : R)
    (hr₂' :
      Membership.mem (γ := Submodule R R)
        (span R (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))) r₂')
    (hr₁ :
      generator
          (span R
            (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)))) =
        r₁ • a + r₂'),
    ∃ (r₁ : R) (r₂ : R),
      d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
⊢ ∃ (r₁ : R) (r₂ : R),
    d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)

Tactic:
obtain ⟨r₁, r₂', hr₂', hr₁⟩ :=
        mem_span_insert.mp (IsPrincipal.generator_mem (Submodule.span R {a, ψ ⟨y, hNO yN⟩}))

Premises used: Insert.insert, Subtype.mk, Submodule.IsPrincipal.generator_mem, Submodule.span, Iff.mp, Singleton.singleton, DFunLike.coe, Submodule.mem_span_insert
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
r₁ r₂' : R
hr₂' :
  Membership.mem (γ := Submodule R R)
    (span R (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))) r₂'
hr₁ :
  generator
      (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)))) =
    r₁ • a + r₂'
obtain :
  ∀ (r₂ : R)
    (hr₂' :
      Membership.mem (γ := Submodule R R)
        (span R (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)))
        (HSMul.hSMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)))
    (hr₁ :
      generator
          (span R
            (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)))) =
        r₁ • a + HSMul.hSMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)),
    ∃ (r₁ : R) (r₂ : R),
      d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
⊢ ∃ (r₁ : R) (r₂ : R),
    d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)

Tactic:
obtain ⟨r₂, rfl⟩ := mem_span_singleton.mp hr₂'

Premises used: Submodule.mem_span_singleton, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
r₁ r₂ : R
hr₂' :
  Membership.mem (γ := Submodule R R)
    (span R (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)))
    (HSMul.hSMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))
hr₁ :
  generator
      (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)))) =
    r₁ • a + HSMul.hSMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
⊢ ∃ (r₁ : R) (r₂ : R),
    d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)

Tactic:
⟨r₁, r₂, hr₁⟩

Premises used: Exists.intro
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
r₁ r₂ : R
hr₂' :
  Membership.mem (γ := Submodule R R)
    (span R (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)))
    (HSMul.hSMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))
hr₁ :
  generator
      (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)))) =
    r₁ • a + HSMul.hSMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
⊢ ∃ (r₁ : R) (r₂ : R),
    d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)

Tactic:
exact ⟨r₁, r₂, hr₁⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
obtain :
  ∀ (r₁ r₂ : R)
    (d_eq : d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)),
    Eq (α := Ideal R)
      (R ∙
        generator
          (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)))))
      (R ∙ generator (ϕ.submoduleImage N))
⊢ Eq (α := Ideal R)
    (R ∙
      generator
        (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)))))
    (R ∙ generator (ϕ.submoduleImage N))

Tactic:
obtain ⟨r₁, r₂, d_eq⟩ : ∃ r₁ r₂ : R, d = r₁ * a + r₂ * ψ ⟨y, hNO yN⟩ := by
      obtain ⟨r₁, r₂', hr₂', hr₁⟩ :=
        mem_span_insert.mp (IsPrincipal.generator_mem (Submodule.span R {a, ψ ⟨y, hNO yN⟩}))
      obtain ⟨r₂, rfl⟩ := mem_span_singleton.mp hr₂'
      exact ⟨r₁, r₂, hr₁⟩

Premises used: Subtype.mk, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
r₁ r₂ : R
d_eq : d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
ψ' : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R := r₁ • ϕ + r₂ • ψ
rw : ∃ (y : M) (yN : y ∈ N), (ψ' : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = d
⊢ R ∙ d ≤ ψ'.submoduleImage N

Tactic:
rw [span_le, singleton_subset_iff, SetLike.mem_coe, LinearMap.mem_submoduleImage_of_le hNO]

Premises used: Set.singleton_subset_iff, LinearMap.mem_submoduleImage_of_le, SetLike.mem_coe, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
r₁ r₂ : R
d_eq : d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
ψ' : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R := r₁ • ϕ + r₂ • ψ
⊢ ∃ (y : M) (yN : y ∈ N), (ψ' : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = d

Tactic:
⟨y, yN, ?_⟩

Premises used: Exists.intro