-- Mathlib/LinearAlgebra/Prod.lean
/-- **Vertical line test** for linear maps.

Let `f : G → H × I` be a linear (or semilinear) map to a product. Assume that `f` is surjective on
the first factor and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` at
most once. Then the image of `f` is the graph of some linear map `f' : H → I`. -/
lemma LinearMap.exists_range_eq_graph {f : G →ₛₗ[σ] H × I} (hf₁ : Surjective (Prod.fst ∘ f))
    (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) :
    ∃ f' : H →ₗ[S] I, LinearMap.range f = LinearMap.graph f'

Proof state:
case h
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ x_1, f x_1 = x) ↔ f' x.1 = x.2
⊢ range f = { toFun := (↑f').toFun, map_add' := ⋯, map_smul' := ⋯ }.graph

Tactic:
ext x

Result:
case h.h
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ x_1, f x_1 = x) ↔ f' x.1 = x.2
x : H × I
⊢ x ∈ range f ↔ x ∈ { toFun := (↑f').toFun, map_add' := ⋯, map_smul' := ⋯ }.graph

Proof state:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ x_1, f x_1 = x) ↔ f' x.1 = x.2
s : S
h : H
⊢ { toFun := (↑f').toFun, map_add' := ⋯ }.toFun (s • h) =
    (RingHom.id S) s • { toFun := (↑f').toFun, map_add' := ⋯ }.toFun h

Tactic:
simp only [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, RingHom.id_apply]

Result:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ x_1, f x_1 = x) ↔ f' x.1 = x.2
s : S
h : H
⊢ f' (s • h) = s • f' h

Proof state:
case h.h
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ x_1, f x_1 = x) ↔ f' x.1 = x.2
x : H × I
⊢ x ∈ range f ↔ x ∈ { toFun := (↑f').toFun, map_add' := ⋯, map_smul' := ⋯ }.graph

Tactic:
simpa only [mem_range, Eq.comm, ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, mem_graph_iff,
  coe_mk, AddHom.coe_mk, AddMonoidHom.coe_coe, Set.mem_range] using hf' x

Result:
no goals

Proof state:
case intro
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ x_1, f x_1 = x) ↔ f' x.1 = x.2
⊢ ∃ f', range f = f'.graph

Tactic:
use
{ toFun := f'.toFun
  map_add' := f'.map_add'
  map_smul' := by
    intro s h
    simp only [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, RingHom.id_apply]
    refine (hf' (s • h, _)).mp ?_
    rw [← Prod.smul_mk, ← LinearMap.mem_range]
    apply Submodule.smul_mem
    rw [LinearMap.mem_range, hf'] }

Result:
case h
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ x_1, f x_1 = x) ↔ f' x.1 = x.2
⊢ range f = { toFun := (↑f').toFun, map_add' := ⋯, map_smul' := ⋯ }.graph