case pos
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsSimpleModule R M
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
h : f = 0
⊢ Function.Bijective ↑f ∨ f = 0

case neg
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsSimpleModule R M
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
h : ¬f = 0
⊢ Function.Bijective ↑f ∨ f = 0
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsSimpleModule R M
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
⊢ Function.Bijective ↑f ∨ f = 0
by_cases h : f = 0
no goals
case neg
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsSimpleModule R M
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
h : ¬f = 0
⊢ Function.Bijective ↑f ∨ f = 0
exact Or.intro_left _ ⟨injective_of_ne_zero h, surjective_of_ne_zero h⟩
case pos.h
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsSimpleModule R M
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
h : f = 0
⊢ f = 0
case pos
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsSimpleModule R M
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
h : f = 0
⊢ Function.Bijective ↑f ∨ f = 0
right
no goals
case pos.h
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsSimpleModule R M
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
h : f = 0
⊢ f = 0
exact h