-- Mathlib/Algebra/Category/Grp/Injective.lean
theorem Module.Baer.of_divisible [DivisibleBy A ℤ] : Module.Baer ℤ A := fun I g ↦ by
  rcases IsPrincipalIdealRing.principal I with ⟨m, rfl⟩
  obtain rfl | h0 := eq_or_ne m 0
  · refine ⟨0, fun n hn ↦ ?_⟩
    rw [Submodule.span_zero_singleton] at hn
    subst hn
    exact (map_zero g).symm
  let gₘ := g ⟨m, Submodule.subset_span (Set.mem_singleton _)⟩
  refine ⟨LinearMap.toSpanSingleton ℤ A (DivisibleBy.div gₘ m), fun n hn ↦ ?_⟩
  rcases Submodule.mem_span_singleton.mp hn with ⟨n, rfl⟩
  rw [map_zsmul, LinearMap.toSpanSingleton_apply, DivisibleBy.div_cancel gₘ h0, ← map_zsmul g,
    SetLike.mk_smul_mk]

Proof state:
case mk.intro.inr.intro
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(Submodule.span ℤ {m}) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := g ⟨m, ⋯⟩
n : ℤ
hn : n • m ∈ Submodule.span ℤ {m}
⊢ (LinearMap.toSpanSingleton ℤ A (DivisibleBy.div gₘ m)) (n • m) = g ⟨n • m, hn⟩

Tactic:
rw [map_zsmul, LinearMap.toSpanSingleton_apply, DivisibleBy.div_cancel gₘ h0, ← map_zsmul g,
  SetLike.mk_smul_mk]

Result:
no goals

Proof state:
case mk.intro.inl
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : ↥(Submodule.span ℤ {0}) →ₗ[ℤ] A
hn : 0 ∈ Submodule.span ℤ {0}
⊢ 0 0 = g ⟨0, hn⟩

Tactic:
exact (map_zero g).symm

Result:
no goals

Proof state:
case mk.intro.inl
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : ↥(Submodule.span ℤ {0}) →ₗ[ℤ] A
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ Submodule.span ℤ {0}), g' x = g ⟨x, mem⟩

Tactic:
refine ⟨0, fun n hn ↦ ?_⟩

Result:
case mk.intro.inl
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : ↥(Submodule.span ℤ {0}) →ₗ[ℤ] A
n : ℤ
hn : n ∈ Submodule.span ℤ {0}
⊢ 0 n = g ⟨n, hn⟩

Proof state:
case mk.intro.inl
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : ↥(Submodule.span ℤ {0}) →ₗ[ℤ] A
n : ℤ
hn : n ∈ Submodule.span ℤ {0}
⊢ 0 n = g ⟨n, hn⟩

Tactic:
rw [Submodule.span_zero_singleton] at hn

Result:
case mk.intro.inl
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : ↥(Submodule.span ℤ {0}) →ₗ[ℤ] A
n : ℤ
hn✝ : n ∈ Submodule.span ℤ {0}
hn : n ∈ ⊥
⊢ 0 n = g ⟨n, hn✝⟩

Proof state:
case mk.intro.inr
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(Submodule.span ℤ {m}) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := g ⟨m, ⋯⟩
n : ℤ
hn : n ∈ Submodule.span ℤ {m}
⊢ (LinearMap.toSpanSingleton ℤ A (DivisibleBy.div gₘ m)) n = g ⟨n, hn⟩

Tactic:
rcases Submodule.mem_span_singleton.mp hn with ⟨n, rfl⟩

Result:
case mk.intro.inr.intro
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(Submodule.span ℤ {m}) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := g ⟨m, ⋯⟩
n : ℤ
hn : n • m ∈ Submodule.span ℤ {m}
⊢ (LinearMap.toSpanSingleton ℤ A (DivisibleBy.div gₘ m)) (n • m) = g ⟨n • m, hn⟩

Proof state:
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
I : Ideal ℤ
g : ↥I →ₗ[ℤ] A
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ I), g' x = g ⟨x, mem⟩

Tactic:
rcases IsPrincipalIdealRing.principal I with ⟨m, rfl⟩

Result:
case mk.intro
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(Submodule.span ℤ {m}) →ₗ[ℤ] A
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ Submodule.span ℤ {m}), g' x = g ⟨x, mem⟩

Proof state:
case mk.intro
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(Submodule.span ℤ {m}) →ₗ[ℤ] A
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ Submodule.span ℤ {m}), g' x = g ⟨x, mem⟩

Tactic:
obtain rfl | h0 := eq_or_ne m 0

Result:
case mk.intro.inl
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : ↥(Submodule.span ℤ {0}) →ₗ[ℤ] A
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ Submodule.span ℤ {0}), g' x = g ⟨x, mem⟩

case mk.intro.inr
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(Submodule.span ℤ {m}) →ₗ[ℤ] A
h0 : m ≠ 0
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ Submodule.span ℤ {m}), g' x = g ⟨x, mem⟩

Proof state:
case mk.intro.inr
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(Submodule.span ℤ {m}) →ₗ[ℤ] A
h0 : m ≠ 0
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ Submodule.span ℤ {m}), g' x = g ⟨x, mem⟩

Tactic:
let gₘ := g ⟨m, Submodule.subset_span (Set.mem_singleton _)⟩

Result:
case mk.intro.inr
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(Submodule.span ℤ {m}) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := g ⟨m, ⋯⟩
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ Submodule.span ℤ {m}), g' x = g ⟨x, mem⟩

Proof state:
case mk.intro.inr
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(Submodule.span ℤ {m}) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := g ⟨m, ⋯⟩
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ Submodule.span ℤ {m}), g' x = g ⟨x, mem⟩

Tactic:
refine ⟨LinearMap.toSpanSingleton ℤ A (DivisibleBy.div gₘ m), fun n hn ↦ ?_⟩

Result:
case mk.intro.inr
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(Submodule.span ℤ {m}) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := g ⟨m, ⋯⟩
n : ℤ
hn : n ∈ Submodule.span ℤ {m}
⊢ (LinearMap.toSpanSingleton ℤ A (DivisibleBy.div gₘ m)) n = g ⟨n, hn⟩

Proof state:
case mk.intro.inl
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : ↥(Submodule.span ℤ {0}) →ₗ[ℤ] A
n : ℤ
hn✝ : n ∈ Submodule.span ℤ {0}
hn : n ∈ ⊥
⊢ 0 n = g ⟨n, hn✝⟩

Tactic:
subst hn

Result:
case mk.intro.inl
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : ↥(Submodule.span ℤ {0}) →ₗ[ℤ] A
hn : 0 ∈ Submodule.span ℤ {0}
⊢ 0 0 = g ⟨0, hn⟩